> 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

Reply via email to