comp.lang.ada
 help / color / mirror / Atom feed
From: Paul Rubin <no.email@nospam.invalid>
Subject: Re: SI Units Checked and Unchecked
Date: Thu, 09 Aug 2018 11:47:11 -0700
Date: 2018-08-09T11:47:11-07:00	[thread overview]
Message-ID: <87sh3ngyxc.fsf@nightsong.com> (raw)
In-Reply-To: aea11f39-b169-4490-a4c7-1306ecbe8e2d@googlegroups.com

"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.

  parent reply	other threads:[~2018-08-09 18:47 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 [this message]
2018-08-09 19:13         ` Dan'l Miller
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