[Haskell-cafe] C functional programming techniques?

[Alexander Solla]

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