Re: SI Units Checked and Unchecked

["Dan'l Miller" <optikos@verizon.net>]

On Thursday, August 9, 2018 at 1:47:15 PM UTC-5, Paul Rubin wrote:
> "Dan'l Miller" writes:
> > Well, factually incorrect opinions like yours above would be the
> > reason for losses similar to the Mars Climate Orbiter in the future,
> > even if coded is so-called ‘safety-critical’ Ada.
> >
> > http://www.cnn.com/TECH/space/9909/30/mars.metric.02
> 
> It looks like traditional

Apparently the “traditional” dimension type of which you speak is weakly typed as a fatal flaw, not strongly typed as I am consistently describing.  The USA's 1707 Queen Anne gallon (and fractions & multiples thereof:  quart, pint, cup, butt) would be strongly-typed as a different type than the 1824 King George so-called Imperial gallon (and fractions & multiples thereof:  Imperial quart, Imperial pint, Imperial cup, Imperial butt), which in turn would be strongly-typed as a different type than the SI liter (and SI prefixes thereof).  Likewise for every other strongly-type unit-of-measure in each widely-utilized system in each dimensionality.

> dimensional analysis wouldn't have helped with
> that.  If you switch feet and meters, they are both units of length, so
> have the same dimensions.

Then that should-have-been-strongly-typed units-of-measure library (or language feature) was maldesigned as merely a weakly-type dimension library (or language feature).

> I get the impression that lots of space stuff is initially coded in
> Matlab and then converted to Ada.  In those cases they probably expect
> Matlab simulations to catch (some of) the bugs.
> 
> > Meticulous typing (especially compile-time enforcement of strong
> > typing) is supposed to be Ada's crowning achievement; C++ or any
> > recent upstart language (e.g., Rust) is not supposed to be able to
> > threaten to usurp the throne from the king on typing-enforcement
> > topics.
> 
> Ada's type system (due to its origins in the 1980s) is decades behind
> current designs.  Ada handles the issue through good integration with
> proof systems like SPARK.

How precisely would SPARK subset & mark-up emulate a strongly-typed units-of-measure capabilities that I describe to catch mixing scalars •implicitly• containing 1707 Queen Anne units of measure or avoirdupois units of measure with scalars •implicitly• containing SI/MKS/CGS units of measure?  That seems quite a stretch for SPARK subset & markup alone to automagically have almost AI-esque ESP insight into what the human-being's meaning of the scalar datum's bits actually semantically mean (without the strongly-typed per-unit-of-measure types that I describe).  Any markup for SPARK to have that deep of a level of insight would be tantamount to a strongly-type units-of-measure library/language-feature capability that would overtly call out Queen Anne's 1707 gallon versus King George III's 1824 gallon versus SI's liter, as I consistently describe.