[email protected]
[Top] [All Lists]

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

Subject: [Haskell-cafe] Re: C functional programming techniques?
From: Maurí­cio CA
Date: Sat, 30 Jan 2010 23:26:13 -0200
>> 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?



Haskell-Cafe mailing list
[email protected]

<Prev in Thread] Current Thread [Next in Thread>