Type Theory and Functional Programming

[Joerg F. Wittenberger]

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.

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.)

> but of course that's not really your problem.
> At any rate, thank you, but please do a little more research before such
> blanket suggestions.

And _please_ be a little more polite with those, who failed to find
everything.  Furthermore, it might have been a suggestion.  Wasn't it?
I'm sorry to say that, but a suggestion should always be welcome.  I
already feel sorry for the TUNES list being not as effective as it
could be, just because the _tone_ is not productive, while the content
is.

Best Regards

/Jörg

> On Fri, 27 Dec 2002, Russell O'Connor wrote:
> 
> > I was browsing the web looking for new OS's when I found your project.
> >
> > I'd like to suggest the book "Type Theory and Functional Programming" by
> > Simon Thompson.  If you want correctness as part your programming
> > language, I think functional style programming with a dependent type
> > system is the way to go.  A dependent type system allows enough
> > expressiveness to make non-trivial claims about program behaviour.  The
> > proof of correctness of code and the code itself is developed
> > simultaneously, and with the same syntax.
> >
> > Good luck with your work.
> >
> > - --
> > Russell O'Connor            <http://www.math.berkeley.edu/~roconnor/>
> 
> -- 
> Brian T. Rice
> LOGOS Research and Development
> mailto:water@tunes.org
> http://tunes.org/~water/

-- 
The worst of harm may often result from the best of intentions.