>> Sorry if this looks weird, but do you know of experiences with
>> functional programming, or "type programming", with C?
> I would use a higher level language to emit valid C. Basically,
> use a strongly typed macro language. "All" you will have to
> prove is that your emitter produces type safe code, which you
> can do by induction and is straight forward.
This is interesting. I wasn't thinking at first about actual
formal proofs, just some way to make small C posix-only programs
easier to read an maintain by using a "big picture" functional
look. But I would like to try that.
Do you have some link to an example of such proof by induction of
Haskell-Cafe mailing list