It doesn't have to be the same metalanguage for every program. You can write your own code generators adapted to the specific problems. They should have a "pi

It doesn't have to be the same metalanguage for every program. You can write your own code generators adapted to the specific problems. They should have a "pit of success", and the knowledge of the domain is used to ensure that. There are few research-level issues here; it's just good engineering. The 0% or 100% mindset is bad engineering. You want something that's short, and that you can explain to other people, and that other people can write an independent implementation of. If the proof is 10x longer than normal code, and it's written in a metalanguage that the relevant people don't know, then it's not very useful. Proofs are not guarantees. CompCERT has had logic bugs despite being written in a formal language. (It does reduce the number of bugs drastically in general, but it's also an extremely expensive technique, and not what I'm advocating.) There are no guarantees in engineering, just good practices. Groveling through bytes one at a time in imperative languages is not an ideal engineering practice, even if the imperative language comes with more guarantees than most.