>> 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 _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
