News for hackers. Stuff that matters.

A comment on CompCert - Compilers you can formally trust. Parent comment

Re:CompCert - Compilers you can formally trust by beza1e1 on Saturday June 04, 2011 @03:20PM (#2620231)
The frontend is not verified. This part parses, checks and lowers C code to a Clight. There is no formal specification of C itself and that would be the first step to verify the frontend.
[ Parent | on HN ]

There are no comments on this comment yet.