It's not a problem at all, it's exactly the direction I'd like to see things go as well. It's just that your code is still a stranger in a strange land in these

It's not a problem at all, it's exactly the direction I'd like to see things go as well. It's just that your code is still a stranger in a strange land in these cases. Your proofs will be full of the typical halmarks of functional programing, and for the stuff that is executed at runtime you'll definitely want some pattern matching, but there will be no closures or higher-order functions and limited opportunities for monads, functors, etc. Would you consider a C program transliterated into a representation of C inside a functional language and then annotated with proofs to be "functional"? My argument is what you get if you write a true kernel (no sitting on top of a runtime written in something else) is going to look a lot like that would.