From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=unavailable autolearn_force=no version=3.4.4 X-Received: by 2002:a1c:9e42:: with SMTP id h63-v6mr390031wme.10.1533841993662; Thu, 09 Aug 2018 12:13:13 -0700 (PDT) X-Received: by 2002:aca:75c9:: with SMTP id q192-v6mr114436oic.3.1533841993232; Thu, 09 Aug 2018 12:13:13 -0700 (PDT) Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!feeder.eternal-september.org!news.gegeweb.eu!gegeweb.org!usenet-fr.net!proxad.net!feeder1-2.proxad.net!209.85.128.88.MISMATCH!z6-v6no5710754wma.0!news-out.google.com!p4-v6ni16514wmb.0!nntp.google.com!g24-v6no15346iti.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Thu, 9 Aug 2018 12:13:12 -0700 (PDT) In-Reply-To: <87sh3ngyxc.fsf@nightsong.com> Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=47.185.195.62; posting-account=zwxLlwoAAAChLBU7oraRzNDnqQYkYbpo NNTP-Posting-Host: 47.185.195.62 References: <9381f30a-a957-4477-b037-b2d60041e83e@googlegroups.com> <87sh3ngyxc.fsf@nightsong.com> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: <5a9e9dbe-479a-49de-a831-5d7bcbc1fa6f@googlegroups.com> Subject: Re: SI Units Checked and Unchecked From: "Dan'l Miller" Injection-Date: Thu, 09 Aug 2018 19:13:13 +0000 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Xref: reader02.eternal-september.org comp.lang.ada:54116 Date: 2018-08-09T12:13:12-07:00 List-Id: 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 =E2=80=98safety-critical=E2=80=99 Ada. > > > > http://www.cnn.com/TECH/space/9909/30/mars.metric.02 >=20 > It looks like traditional Apparently the =E2=80=9Ctraditional=E2=80=9D dimension type of which you sp= eak is weakly typed as a fatal flaw, not strongly typed as I am consistentl= y describing. The USA's 1707 Queen Anne gallon (and fractions & multiples = thereof: quart, pint, cup, butt) would be strongly-typed as a different ty= pe than the 1824 King George so-called Imperial gallon (and fractions & mul= tiples thereof: Imperial quart, Imperial pint, Imperial cup, Imperial butt= ), which in turn would be strongly-typed as a different type than the SI li= ter (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 lang= uage 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. >=20 > > 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. >=20 > 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-o= f-measure capabilities that I describe to catch mixing scalars =E2=80=A2imp= licitly=E2=80=A2 containing 1707 Queen Anne units of measure or avoirdupois= units of measure with scalars =E2=80=A2implicitly=E2=80=A2=C2=A0containing= 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 ta= ntamount to a strongly-type units-of-measure library/language-feature capab= ility that would overtly call out Queen Anne's 1707 gallon versus King Geor= ge III's 1824 gallon versus SI's liter, as I consistently describe.