[m-users.] A more precise determinism checker

Zoltan Somogyi zoltan.somogyi at runbox.com
Sun Mar 20 18:00:41 AEDT 2022


2022-03-20 17:30 GMT+11:00 "Richard O'Keefe" <raoknz at gmail.com>:

Nice to hear from you again, as always.

> If I may take the liberty, I'd like to paraphrase part of what
> I understand Zoltan to be saying:
>  - as a rule, you get a particular determinism in Mercury
>    because that is the determinism you *intend* to get,
>  - we programmers need to understand the connection between
>    what determinism we intend to get and how to get it,
>  - if the compiler's rules are too complex, *we* won't
>    understand them, and will be left poking hopelessly at
>    the code hoping the error message will go away.

My main message was your third point, which as a sort-of corollary
requires your point 2, except your explanation is much clearer than mine.

A real life example of "poking hopelessly at the code" of a system
you don't understand, look at the woes of Tesla's so-called Full Self
Driving software (which is full-self-driving ONLY in the sense that
legally, you, the owner, have to fully drive your car yourself :-().
The "code" in this case consists mainly of a set of machine learning systems
that were not written by humans at all, so you can't understand it by asking its
authors. And in their case, the "error messages" take the form
of video recordings and telemetry records from situations in which
the FSD system tried to steer the Tesla and its occupants into a collision.

I was not making the argument in your point 1. I was saying rather
that the compiler will compute the determinism for your code
that your code deserves. That will be the determinism you intend
only if your code did not have a bug :-(

> I will say that there are some application areas where high
> levels of compile-time checking are worth it.  I am talking
> to some people about a multi-year nationally distributed embedded
> system, and I am trying to persuade them that the costs of
> bugs in *this* environment make SPARK+Ada the right choice at
> the edge, but it's hardly a typical application domain.

If you need additional ammunition for your argument, you may
want to bring up the huge cost overruns on the software for the F-35.
The US DoD created Ada for the express purpose of improving
the reliability of their software, mandating its use in all software
written for them, but then starting giving out waivers permitting
the use other languages, mainly C++, first for a few projects,
then for pretty much all projects. The result was a huge series
of software messes costing billions of dollars of extra cost and
years of delay. At least the firms that wrote that software did save
the few million dollars that they would have had to spend training
the C++ programmers they hired off the street how to program
in Ada :-(

Zoltan.


More information about the users mailing list