COGENT takes pretty much precisely the approach I described below: it uses domain-specific structures in a functional language to encode verified imperative cod

COGENT takes pretty much precisely the approach I described below: it uses domain-specific structures in a functional language to encode verified imperative code. If you look at pretty much any code in the ext2 pilot (here[1] is as good as any) you'll notice that a lot of the functions called are things like destroy_Ext2DirEnt (which unless they named things poorly, takes a clear action), as well as a lot of passing around of memory addresses to functions that write them (e.g. deserialise_Ext2DirEnt2). It's not that they wrote the logic in a fundamentally different paradigm from C, it's that they take care to give their system the information it needs to both generate C code and most of the desired proofs simultaneously. The functional language is fufilling the role of metalanguage excellently, but little of that ends up in the generated code. The one functional thing that does is pattern matching, since the C equivalent (if statements and unions) are much harder to verify (and use). [1]: https://github.com/NICTA/cogent/blob/master/impl/ext2/cogent/src/dread.cogent https://github.com/NICTA/cogent/blob/master/impl/ext2/cogent...