From: "M. Edward (Ed) Borasky" <znmeb@...>
Date: 2006-08-09T13:22:54+09:00
Subject: Re: Language chatter

gabriele renzi wrote:
> notice that to proof some properties of a program you don't 
> necessarily need a functional language.
> For example, you may love to take a look at Spark[1], a statically 
> verifiable subset of Ada, or at Vault[2].
IIRC the *original* exercise in proving a program correct was in fact 
not for a functional language, but for a flowchart. Was it Floyd??


> Other languages can proof correctness for "some"functionalities.
> I had the chance to work with NesC[3] wich is a nifty language for 
> embbeded systems, basically C+concurrency+components, where the 
> compiler checks that there are no race conditions in concurrent code 
> (it gets some false positives, but no wrong code passes).
I think my philosophy boils down to this:
1. A false positive -- an indication from the tool that a program 
contains a race when it in fact does not -- is an indication that the 
program is too difficult to read and should be rewritten so it generates 
a true negative.
2. By the same token, failure of the verifying tool to prove correctness 
of a program in an economically viable amount of time should also be 
taken as an indication that the program is too difficult to read and 
should be rewritten.