cogent

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

The cogent language by nicta (an easy google away) has functional semantics but uses linear logic / linear types to make sure that no gc is needed. The code is on github and they have a very cool approach to generating proofs that any code generation maps the cogent code to equivalent c code. https://github.com/NICTA/cogent/tree/master/cogent I've also been looking into how to add resource logic / linear logic to ghc Haskell / languages with a similar internal rep as ghc core. Still need to write that stuff up mind you. There's a long history of no gc free functional language research. Mlkit and clean are probably two of the older but accessible implementations in the wild