Type Theory and Functional Programming
Joerg F. Wittenberger
Joerg F. Wittenberger" <Joerg.Wittenberger@pobox.com
Sat Mar 15 04:15:02 2003
> 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
> 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
The worst of harm may often result from the best of intentions.