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's promising for same reason Rust having no GC is. :)
re Frama-C. Oh, yeah, that's good thinking as it'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'm not formal methods specialist. Anyway, you might like where such techniques got their start for mainstream languages:
Thanks for the link. I really appreciate HP has kept DEC papers alive, they are my main source into Modula-3 universe, but they are hard to search for.
Another possibility using something like the "Tiger book" and write a ML -> C compiler for the C subset you care about, but by then maybe contributing to Ada (GNAT), Rust or Swift would be better use of time.
I also forgot to mention on my previous comment that Idris and F* also have C backends, but they might suffer from the same problems.
As I suspected. Thanks for the confirmation. I'm guessing human-readable output might have to be done at an earlier stage in the compiler to keep it close to original code. Or do it high-assurance style with each intermediate representation in C to let reader see what transformed code means.
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's promising for same reason Rust having no GC is. :)
re Frama-C. Oh, yeah, that's good thinking as it'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'm not formal methods specialist. Anyway, you might like where such techniques got their start for mainstream languages:
http://apotheca.hpl.hp.com/ftp/pub/dec/SRC/research-reports/...