From: "Dan'l Miller" <optikos@verizon.net>
Subject: Re: SI Units Checked and Unchecked
Date: Thu, 9 Aug 2018 12:13:12 -0700 (PDT)
Date: 2018-08-09T12:13:12-07:00 [thread overview]
Message-ID: <5a9e9dbe-479a-49de-a831-5d7bcbc1fa6f@googlegroups.com> (raw)
In-Reply-To: <87sh3ngyxc.fsf@nightsong.com>
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.
next prev parent reply other threads:[~2018-08-09 19:13 UTC|newest]
Thread overview: 33+ messages / expand[flat|nested] mbox.gz Atom feed top
2018-08-09 12:44 SI Units Checked and Unchecked AdaMagica
2018-08-09 13:47 ` Dan'l Miller
2018-08-09 14:07 ` Dmitry A. Kazakov
2018-08-09 15:03 ` Dan'l Miller
2018-08-09 15:51 ` Dmitry A. Kazakov
2018-08-09 17:32 ` Dan'l Miller
2018-08-09 19:42 ` Dmitry A. Kazakov
2018-08-09 22:12 ` Dan'l Miller
2018-08-10 6:45 ` Dmitry A. Kazakov
2018-08-10 13:59 ` Dan'l Miller
2018-08-10 14:50 ` Dmitry A. Kazakov
2018-08-10 17:04 ` Dan'l Miller
2018-08-10 17:34 ` Dmitry A. Kazakov
2018-08-11 4:42 ` Paul Rubin
2018-08-11 5:46 ` Dmitry A. Kazakov
2018-08-11 19:57 ` Paul Rubin
2018-08-11 21:01 ` Dmitry A. Kazakov
2018-08-09 18:47 ` Paul Rubin
2018-08-09 19:13 ` Dan'l Miller [this message]
2018-08-09 14:31 ` AdaMagica
2018-08-09 15:19 ` Dan'l Miller
2018-08-09 16:07 ` Jeffrey R. Carter
2018-08-09 17:41 ` AdaMagica
2018-08-09 20:34 ` Jeffrey R. Carter
2018-08-10 9:13 ` AdaMagica
2018-08-10 20:20 ` Jeffrey R. Carter
2018-08-13 8:57 ` AdaMagica
2018-08-20 17:55 ` AdaMagica
2019-09-04 14:20 ` Shark8
2019-09-04 17:11 ` AdaMagica
2019-09-06 21:01 ` Shark8
2020-08-13 12:24 ` SI Units Checked and Unchecked - Completela overhauled version AdaMagica
-- strict thread matches above, loose matches on Subject: below --
2003-02-05 7:03 SI Units Checked and Unchecked Grein, Christoph
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox