Type Theory and Functional Programming

[Tom Novelli]

On Sun, Mar 16, 2003 at 04:30:12AM -0800, Brian T Rice wrote:
> On 15 Mar 2003, Joerg F. Wittenberger wrote:
> 
> > Hi Brian,
> >
> > > While this is a reasonable suggestion, functional programming as you
> > > describe it is not useful enough for Tunes. The current website doesn't
> > > make this explicit enough,
> >
> > It would be _really_ useful, if the website could make the _reasons_
> > explicit, why functional programming is not useful enough.
> 
> The simple fact that we need to express Active objects with side-effects
> or lots of dynamic annotations within the language should be reason
> enough. No monad or co-monad or dyad or whatever is ever going to be a
> final answer to this.
> 
> > There is a nice article - I can't find the reference right now - which
> > basically shows that the only difference between functional and
> > non-functional programming is the fact that the former can proof their
> > results, while the latter can't.  I do have the feeling that our
> > mathematics is just the way it is, because over the thousends of
> > years, we never found a better theory.  Hence I'm very sceptical, when
> > there is a note like "not enough" towards math.  (I'm not saying you
> > are wrong, I just say: please proof you statement.)
> 
> Well, if you define "functional programming" as "any language whose
> programs you can prove" then your statement is trivially true, but that's
> an entirely false concept. There are plenty of languages which are /not/
> functional that have provable qualities, and even express side-effects. I
> speak mainly about Maude, but there are other similar rewrite languages
> which have this property.

There was a provable assembler written at Cornell.  It's provable because
it's typed, and it's not "functional".  Caveat: that's what the authors
claimed... it may be flawed or just too damned awkward (exponentially more
so than standard assembler :)

Let's do a few litmus tests on any "functional" or "provable"
language/system.  Can you write a simple text editor, task scheduler, and
disk driver?  Using straightforward, concise, readable, maintainable code? 
If the answer is a definite "yes" all around, you have a winner.  Otherwise,
forget it; the world has enough computer fiascos already.

I'm skeptical of this whole idea of automatic proof.  I think the principle
is, any system complex enough to be useful will be unprovable within itself. 
Anyone could tell you that's common sense, but it took guys like Godel to
prove it.  But I'll withhold judgement for now, since I'm no expert, and I
wish you luck.

Tom Novelli