Micro-overview: research project that treats each core independently with message passing between them. Lots of interesting implementation stuff, e.g. "Barrelfish makes extensive use of DSLs for generating low-level operating system code in C", and they have a correctness proof for that framework, which is written in Haskell.