Re: "foundations built on sand"
Dear All, regarding:
> 1) ML was developed triggered by "foundational" work on PCF
> (at least that's how it appears to me from my fairly incomplete
> record of history)
I am not quite sure what Thomas means here, although ML and PCF are
certainly both part of a certain common thread of ideas and development.
Milner was involved in both, but I never heard suggestions before of a
direct influence. My understanding is that ML started with the need for
a metalanguage for LCF, and was influenced by LISP, ISWIM and POP2. The
need for a metalanguage for LCF forced a type discipline on the
language, viz. ML polymorphism.
Certainly, though, semantical and type-theoretic ideas have been
instrumental in the development of ML. For example, see Karen Frenkel's
interview with Robin Milner in CACM, Vol. 36, No. 1, 1993. Milner
stresses there the simultaneous development of the design of the
language, its implementation and its formal definition. Another place to
look for the history of ML is "The Definition of Standard ML (Revised)"
by Milner, Tofte, Harper and MacQueen.
Best, Gordon Plotkin