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

[Vinzent Hoefler]

On Tuesday 14 August 2007 08:08, Florian Klaempfl wrote:
> Vinzent Hoefler schrieb:
> > 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
>
> As long as they can't prove that Goedel is wrong I don't believe in
> it :)

Well, I've seen it in action. And I don't see the reference to Goedel 
here. Basically it's predicate logic, which is - according to Goedel - 
both complete and correct.

Of course, they can't solve the halting problem. But most systems they 
design are not designed to halt, anyway. ;)


Vinzent.