>>105564145
>Is it really that high of a skill barrier?
no, it's just a lot of work.
also if you really want to go this route, the best option for real (though not real-time) work is idris
https://www.idris-lang.org/
there are problems with formal verification by the way
https://spinroot.com/spin/Doc/rax.pdf
tl;dr formally verified system failed because of an issue with the spec
the more complicated the thing you're working on (operating systems are VERY complicated) the more holes and contradictions there are going to be in your spec, and you end up playing conceptual jenga as you try and work out the kinks. small changes turn into huge refactors and architectural re-thinking.
it's "doable" but you need a lot of really good people working over a long period of time, and that's not cheap.
