[Drup]

> Its small size serves both its aspirations of correctness ...

No, a compiler (hell, a software) written in C is not correct, period. If you want a C compiler that has slight chances to be correct, you use compcert.

The small size is an awesome property for education (both for the writer and the reader). For this purpose, it's absolutely great, so kudos for that. :)

[mpu]

At least, I can try!

And also, we are seeing more and more certified C programs: see the DeepSpec NSF expedition grant, the Verified Software Toolchain, and the CertiKOS project for examples. I work with these guys.

[nickpsecurity]

You are soooo lucky. DeepSpec has a near dream team of people working on this issue. Appel and Chlipala alone could probably knock out most of the problem given enough time. Add the others and great stuff on publication list is entirely unsurprising. Except in its cleverness. :) Glad you brought it up as I haven't read the info flow for c & asm paper yet.

Btw, hows progress coming on those projects? Specifically, are any of the tools (a) useful for non-experts with a little bit of training by tutorials, etc and (b) available for download in open-source or binary form yet? Thanks ahead of time.

[andrewchambers]

Not to mention qbe is much faster than both clang and gcc when it comes to compiling things.