[FOM] Re: 187:Grand Unification 2 - saving human lives

[Till Mossakowski]

Harvey Friedman wrote:

> What is needed is an appropriate mathematically friendly functional 
> programming language, with clear mathematically friendly semantics, 
> which does not sacrifice much in the way of efficiency. Complete 
> modularity, no side effects, where semantics is inherited from the 
> standard semantics of mathematics, etc. It should be noted that there 
> are plenty of important contexts in which efficiency is not even 
> remotely at issue but correctness and specification is - for example, in 
> the area of the design and implementation of complex user interfaces.

What about Haskell?
It is pure, no side effects, and has an elegant encapsulation of
stateful computations via monads. Moreover, non-trivial programs
(also system programs) have been written in Haskell.
The semantics being "inherited from the standard semantics of mathematics"
is a bit difficult in presence of polymorphic datatypes and general
recursion (which can hardly be omitted), but I think that one can say
that it comes close to that.

See www.haskell.org

I should also mention the work of our group on reconciling Haskell
semantics with the Henkin-style model theory of higher-order logic:

http://www.informatik.uni-bremen.de/~till/papers/hascasl.ps.gz
http://www.informatik.uni-bremen.de/~till/papers/pdlJournal.ps.gz

Till Mossakowski


-- 
Till Mossakowski               Phone +49-421-218-4683
Dept. of Computer Science      Fax +49-421-218-3054
University of Bremen           till at tzi.de
P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till