3 ms·
There many attempts to get proofs for compilers for popular languages, C or Ada for example: http://portal.acm.org/citation.cfm?id=1315602 http://portal.acm.org
by ilkhd2 17y ago
There many attempts to get proofs for compilers for popular languages, C or Ada for example:
http://portal.acm.org/citation.cfm?id=1315602 http://portal.acm.org/citation.cfm?id=1315602
http://pauillac.inria.fr/~xleroy/publi/compiler-certif.pdf http://pauillac.inria.fr/~xleroy/publi/compiler-certif.pdf
- daeken 17y agoYes, I'm aware. However, like most such things, they're simply not practical. Proving compiler correctness is insanely difficult (if it wasn't, we'd have much better compilers) and it very frequently ignores optimization entirely, making such compilers useless. In theory, proving correctness is a good way to go. In the real world, it's not remotely viable.