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