News for hackers. Stuff that matters.

A comment on Proving a Computer Program's Correctness. Parent comment

Re:Proving a Computer Program's Correctness by billswift on Friday October 02, 2009 @11:34AM (#857252)
The language specification and the compiler would have to be proven correct first. Which is increasingly difficult with higher level languages and with optimizing compilers. The critical aspect is that the MACHINE CODE has to be correct. That is one of the reasons the problem is so hard.
[ Parent | on HN ]
Re:Proving a Computer Program's Correctness by gdp on Friday October 02, 2009 @11:50AM (#857291)
For this project, that's assumed. Provided you have some kind of formal semantics, you can define translations. And in fact, Adam Chlipala's work on certified compilers show that it's not impossible.

http://adam.chlipala.net/papers/CtpcPLDI07/

(there are subsequent papers too, but that's probably a good place to start).

[ Parent | on HN ]