On Jan 29, 2010, at 9:11 AM, Maurí cio CA wrote:
Sorry if this looks weird, but do you know of experiences with functional programming, or "type programming", with C? Using macro tricks or just good specifications?
I know this is not absurd to a small extent. I've heard of proof tool certificated C code on the net (although I don't understand that theory), and I was also able to use what I learned from Haskell in a few C-like tasks. [*]
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. You can build up a small library of combinators for type safe units of C code. Haskell might be a good choice for writing your C pre-processor, but there are plenty of choices. Using something like ehaskell (or eruby) might be a good approach. http://hackage.haskell.org/package/ehaskell