Hacker News Reader

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://pauillac.inria.fr/~xleroy/publi/compiler-certif.pdf

View on HN

Yes, 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.

Reply on news.ycombinator.com