I want a Coq kernel! But seriously, I'm not sure writing the stuff in assembly can also optimise simplicity and manageability. Though we are talking about the

I want a Coq kernel! But seriously, I'm not sure writing the stuff in assembly can also optimise simplicity and manageability. Though we are talking about the obsolete X86 architecture here. More reasonable hardware[1] will likely be easier to compile to. [1]: http://millcomputing.com/ http://millcomputing.com/