[Haskell-cafe] Re: [Haskell] [Fwd: Re: Computer Language Shootout]

[Andrzej Jaworski]

On 2/26/07, Kirsten Chevalier honored me with his attention:

>Can you clarify what you mean by this? How do you formally prove that
>a programming language (rather than a specific implementation of one)
>performs better for a given problem? (..)

It is about my saying:"SML was exhaustively proved to predict this logic
much better."

Formal proof requires a theory. So you might use Copernicus model to
formally prove that Australia is on the other side of  Earth against Europe.
Exhaustive prove might require you to dig a very deep hole in the
ground;-)
In case of proving softspots of Haskell, a couple of very knowledgeable
people here and there dug through exhaustive set of alternatives. That's it.

In case of formal proves over programming languages aspirations are limited
to program correctness and probably will never address performance. (see
http://unit.aist.go.jp/cvs/Agda/)

Unfortunately I spend most of my time doing first kind of proofs, I am not
sure how it is with you;-)

>I've read a few of your posts and I still don't understand what you
>mean by a compiler "address[ing] specific properties of a program".
>Can you give an example of the kinds of program properties you're
>talking about, and explain how C compilers exploit them in a way that
>Haskell compilers currently fail to do?

My posts were intentionally motivational because I wanted to get feedback on
the problem.
As to "address[ing] specific properties of a program".
In ADP a program deals with DNA and molecular structures. Because the
program is a sort of inference engine and simulator at the same time it is
desirable to introduce likelihood function as low as possible to avoid
blowing up search spaces when everything is constructed and reconstructed at
the same time. C is low so that's it. However that is done at a cost - the
routines that access the pre-calculated data are no longer identical to
those that access the routines that initially calculated the data. In Prolog
or Haskell they could remain the same.

Have a good time,
-Andrzej