> On May 25, 2023, at 3:30 PM, Chuck Guzis via cctalk <cctalk@classiccmp.org>
> wrote:
>
> On 5/25/23 10:06, Guy Sotomayor via cctalk wrote:
>>
>
>> The way SPARK works is that you have code and then can also provide
>> proofs for the code. Proofs are you might expect are *hard* to write
>> and in many cases are *huge* relative to the actual code (at least if
>> you want a platinum level proof).
>
> ...and we still get gems like the Boeing 737MAX...
>
> --Chuck
Yes. The problem is the gap between informal understanding and formal
description. For many programmers, that gap occurs when the program source is
created. If the programs are subjected to formal proofs, the gap occurs when
the formal specs are written.
So such things are largely a non-solution. They may help a little if the gap
to the formal spec is smaller. If, as Guy is saying, the formal spec is larger
than the code, then obviously that won't be the case.
Languages other than C and C++ have advantages in that they detect, or avoid, a
whole lot of bugs that C/C++ ignore, like bounds violations or memory leaks.
So Ada can be helpful in that some bugs are harder or impossible to create, or
more likely to be detected in testing. But, in spite of having taken a very
interesting week-long course on program proofs by pioneer E.W. Dijkstra, I
don't actually believe in those things.
The 737MAX is a classic example of designers turning off their brains before
doing their work. It is obvious even to me (who have never created
safety-sensitive software) that you don't attach systems with single points of
failure such as non-replicated sensors to a control system whose specific
purpose is to point the airplane nose DOWN. If you do your work with your
brain disabled you can't produce correct software, with or without formal
proofs.
paul
