[fpc-pascal] Competitive advantage in showing proof of correctness

[Vinzent Hoefler]

On Tuesday 14 August 2007 06:14, Daniël Mantione wrote:

> Lastly, pre and post conditions are just another runtime check.

No. If you can prove that the conditions always hold, you don't even 
need to compile to the program to prove its correctness.

There's a company already doing that:

http://www.praxis-his.com/sparkada/intro.asp

Unfortunately the language is rather limited in terms of dynamic, 
hard-to-prove constructs like exceptions, pointers or gotos.


For the ones who are interested, according to Lockheed:

- Code quality improved by a factor of 10 over industry norms for
  DO 178B Level A software.
- Productivity improved by a factor of 4 over previous comparable
  programs.
- Development costs half of that typical for non safety-critical code.

  -- http://www.praxis-his.com/sparkada/pdfs/spark_c130j.pdf

The most interesting sentence is probably the last. Doing it correct 
right from the start is actually cheaper.


Vinzent.