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

[Daniël Mantione]

Op Mon, 13 Aug 2007, schreef JK Smith at Grid-Sky:

> As I mentioned before, assuming some degree of liability for your work is on
> the horizon.
> 
> From
> http://www.lightbluetouchpaper.org/2007/08/10/house-of-lords-inquiry-personal-internet-security/
> 
> Quote:
> 
> "The third area, and this is where the committee has been most far-sighted,
> and therefore in the short term this may well be their most controversial
> recommendation, is that they wish to see a software liability regime, viz:
> that software companies should become responsible for their security
> failures....
> 
> "...in practice it may be a decade or two before there's sufficient case law
> for vendors to know quite where they stand if they ship a product with a
> buffer overflow, or a race condition, or just a default password."
> 
> This will be a major opportunity to be exploited by a vendor who can design
> apps which show due diligence via Contract Programming.

Let's first get people of type unsafe languages. Type safety with range 
checking etc. are a big improvement over type unsafe languages. Yes, 
Pascal is already the language to use if you are interrested in software 
correctness.

And perhaps Tom Verhoeff's work will lead to contract programming. But I 
don't believe it will be a requirement for FPC, as after decades, very few 
people have an interrest in correctness of their programs. Lastly, pre and 
post conditions are just another runtime check. Checks can be used to show 
the existance of bugs, but not their absence.


Daniël