Thanks for links. So, here we go.<p>re generating C. The key thing is whether it generates human-readable and -editable C. Most of those tools are used to just feed and piggyback on a C compiler. In my scheme, the Haskell is like the high-level, executable spec with C being equivalent. Such tools might be a start on my goal. I like that JHC has no garbage collector. That&#x27;s promising for same reason Rust having no GC is. :)<p>re Frama-C. Oh, yeah, that&#x27;s good thinking as it&#x27;s already been used for plenty C verification, even standard library. I was thinking of encoding Haskell specs in Frama-C somehow but not sure as I&#x27;m not formal methods specialist. Anyway, you might like where such techniques got their start for mainstream languages:<p><a href="http:&#x2F;&#x2F;apotheca.hpl.hp.com&#x2F;ftp&#x2F;pub&#x2F;dec&#x2F;SRC&#x2F;research-reports&#x2F;SRC-159.pdf" rel="nofollow">http:&#x2F;&#x2F;apotheca.hpl.hp.com&#x2F;ftp&#x2F;pub&#x2F;dec&#x2F;SRC&#x2F;research-reports&#x2F;...</a>