5 ms·
If a program is formally proven to be correct, it doesn't matter what language it's written in.
by jude- 12y ago
If a program is formally proven to be correct, it doesn't matter what language it's written in.
- ef4 12y agoAgreed, but that's not what they did here. They didn't prove the program is correct, they proved the algorithm is correct. It remains to be seen how closely the program actually implements the algorithm in the paper.
- rational-future 12y agoI guess you missed the /s at the end. As the perfect program runs on top of buggy hardware, OS, libraries, VMs, etc.
- jroesch 12y agoLanguage choice can be important. If you do the common thing and build a distinct model of your program and prove it correct your guarantees don't hold about the actual implementation. You need a second method to ensure equivalence between your model and implementation, this obviously requires much more work and can vary greatly based on the tools and programming languages involved.
- jude- 12y agoYes--choose the language and development process that makes it easiest to reason about the desired properties of the program. Example: seL4 is written in C (as in, written by hand by fallible humans--not compiled down from a higher-level language [1]). But, the C is written in such a way that it is feasible to prove its equivalence to a Haskell prototype which had previously been proven correct. Yes, language choice can be important. But, the degree of its importance depends on what you're building with it and how you're using it. [1] http://www.nicta.com.au/pub-download/full/7371 http://www.nicta.com.au/pub-download/full/7371