[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-pers=
onal-internet-security/
> =

> Quote:
> =

> "The third area, and this is where the committee has been most far-sighte=
d,
> 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 desi=
gn
> 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=EBl