30 Jan
2010
30 Jan
'10
8:26 p.m.
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