2 ms·

If you haven't done so, you might want to look at some of the work done by the seL4 microkernel project. They start with a Haskell prototype that is translated

If you haven't done so, you might want to look at some of the work done by the seL4 microkernel project. They start with a Haskell prototype that is translated programatically into a formal specification for the theorem prover. They then implement the same thing in C, and use a refinement prove to demonstrate that it matches their Haskell implementation. They then compile the program, and create another refinement proof to demonstrate that the binary code matches the C semantics.

nanolith 2y ago
I'll refer you to my reply to a sibling comment. I'm hoping that I can build a more efficient means of doing similar work as with seL4, but without the 30 man year effort. They are on the right track. But, I think there have been some improvements since their effort that can lead to more streamlined equivalence proofs.