On Wed, Mar 10, 2010 at 7:03 PM, Jonathan S. Shapiro <[email protected]> wrote: > Just went back to see what the state of C-- is these days. Regrettably it > seems like something we shouldn't use, for two reasons: > > 1. The discussion list is nearly idle. > 2. The only current implemenation relies on ML, which seems like a bad > dependency for us.
There is also Clight, a large subset of C, an INRIA project led by Xavier Leroy, of Ocaml fame. It is part of the project CompCert which aims to build a formally verified compiler. It's operational, and large parts are verified, I believe. There was a survey article in a recent CACM (July 2009). They even have safe code optimizers, using a "verified validator" approach (the optimizer program itself is not verified, but each optimized output is checked at runtime to be semantically equivalent to the input using a small validator that has been formally verified). This paper is a must read. http://cacm.acm.org/magazines/2009/7/32099-formal-verification-of-a-realistic-compiler/abstract > LLVM, by contrast, is alive, well, and implemented in an unsafe language. Oh > well. There is HLVM, based on LLVM, that aims to support higher-level languages. It has been used as a target for Ocaml. http://www.ffconsultancy.com/ocaml/hlvm/ The project is ambitious and might therefore be a bit risky to choose as a "stable" target for BitC backend development. But it appears to have been going somewhere pretty quickly. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
