I am a huge fan of mm0, the thesis[0] is so brilliantly written, and MMC is such a great step towards the kind of verified computing I really want to be doing
Huh I hadn't paid that much attention to MMC, but this looks fascinating! I don't like how fragile SMT servers are, so to be able to use tactics and proof techniques would be really powerful for formal verification. Also, to be able to prove properties about pointers would let me check some of my work with non-tree data structures.