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
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: Paul Rubin <no.email@nospam.invalid>
Newsgroups: comp.lang.ada
Subject: Re: SI Units Checked and Unchecked
Date: Thu, 09 Aug 2018 11:47:11 -0700
Organization: A noiseless patient Spider
Message-ID: <87sh3ngyxc.fsf@nightsong.com>
References: <9381f30a-a957-4477-b037-b2d60041e83e@googlegroups.com>
	<d628e94f-7ea0-4616-96a9-eb28ff6c9d6e@googlegroups.com>
	<pkhhqo$4d8$1@gioia.aioe.org>
	<aea11f39-b169-4490-a4c7-1306ecbe8e2d@googlegroups.com>
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: 8bit
Injection-Info: reader02.eternal-september.org;
 posting-host="1f7f4b10c155f3e71b8035b91eaba189";
	logging-data="3742"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX1/yMLQvSsycUkUAo2A/zVAD"
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.3 (gnu/linux)
Cancel-Lock: sha1:c0oRuc8AGTgcDadhX+bdm+1X9a4=
	sha1:BLsYgFcrldDBNsnB+TELKUYssss=
Xref: reader02.eternal-september.org comp.lang.ada:54115
Date: 2018-08-09T11:47:11-07:00
List-Id: <comp.lang.ada>

"Dan'l Miller" <optikos@verizon.net> 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 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.

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.  That seems like a fine approach.

This exercise is probably doable in Ada though:

http://blog.tmorris.net/posts/understanding-practical-api-design-static-typing-and-functional-programming/

It was pretty easy in Haskell.