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. _______________________________________________ fpc-pascal maillist - fpc-pascal@lists.freepascal.org http://lists.freepascal.org/mailman/listinfo/fpc-pascal
