Lambda the Ultimate

Impossible? Had we not designed compilers, operating systems, and document editors in small teams? And had I not repeatedly experienced that an inadequate and frustrating program could be programmed from scratch in a fraction of source code used by the original design? Our brain-storming continued, with many intermissions, over several weeks, and certain shapes of a system structure slowly emerged through the haze. After some time, the preposterous decision was made: we would embark on the design of an operating system for our workstation (which happened to be much less powerful than the one used for my rectangle-pushing) from scratch.

Download the PDF edition of this classic book today!

via Heiko Wengler in the discussion forum. (Thanks!!)

I've been doing a lot of (g)awk lately and recently stumbled upon an interesting little paper called GAWK for AI?.

This resonates with my recent experiences/revelations regarding how feature impoverished languages (like gawk) can often help you focus more on the domain and task at hand.

Xavier Leroy's contribution to POPL'06 is Formal certification of a compiler back-end, or: programming a compiler with a proof assistant, which describes a fairly realistic mini-compiler from a subset of C, called Cminor, to PPC assembler.

So what? It's written entirely in Coq, which pretty much makes a certified compiler for free, and all done in a particularly easy way to leverage if you want to show particular implementations correct.

He's got a resource page up with the implementation (which he calls CompCert), and some further notes.