[Haskell-cafe] Re: C functional programming techniques?

[Maurí­cio CA]

 >> 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
type safety?

Thanks,

Maurício