This seems like a well-articulated point, written with a civil tone. Rather than downvoting, perhaps people could make a counter-argument? The approach of "thin

This seems like a well-articulated point, written with a civil tone. Rather than downvoting, perhaps people could make a counter-argument? The approach of "thinking and getting things right" before writing code might not be common with this audience, but there are fields where it's the only way to work. I think the idea of compile-time safety proofs is interesting. The number of runtime cycles spent on policy enforcement could be greatly reduced. Would it ever be possible, though, to derive such proofs for programs written in "unsafe" languages, or for arbitrary binaries? An OS which only supports one language would be unlikely to be generally useful, although it might provide sufficiently compelling benefits for specialized use cases. I believe MirageOS represents an OCaml implementation of this idea, although it may in fact support other languages.