From: Robin M. <Rob...@cl...> - 2001-10-06 12:06:32
|
Dear sml-implementers Since my last message to the implementers list, I've seen contributions by Mads Tofte, Dave Berry and Bob Harper. I would like to comment on these. Before doing so, let me say again that I greatly value the development of ML. The fact that we disagree over the way to do it doesn't diminish the importance of doing it. Mads says "I think it reasonable that the onus is on those who want change". I fully agree with this, and below I try to say what I think this means. I go along with a lot of what Dave Berry says in his careful message. I won't comment in detail, but hang my response on one of his paragraphs: So can we find a common ground in which we can evolve "Standard ML" without risking the problems that you warn of? (Assuming that the implementers can reach agreement between ourselves, of course, which is yet to be proven). I think we can: the key is to minimise the risks to stability, to manage expectations, and to clearly delineate authorship. It's here that I disgree. Instead of "I think we can" I would say "I shall not believe so until I see it". That is not to criticise any of those aiming to do it; but it does firmly say that the onus is on those who want change. I have seen nothing to suggest that those who want change agree on what they want (even when they _seek_ to agree); in the development of the Definition --which by the way was coordinated with implementers-- we often found that seemingly small differences over seemingly small matters grew quite unexpectedly, and consumed a great deal of effort. The only evidence of consensus will be the delivery of what Dave calls a de facto revision of Standard ML, completed and tied in well with the existing Definition. Those embarking on this exercise, which I think is a worthy one, must therefore call it something different from Standard ML; when they have completed it, the rest of the community is free to accept it or not. I thank Bob Harper for his tribute to my past efforts. It's a good time for me also to thank all those who took part in defining, implementing and promulgating SML, and made it work so well in spite of their differences. I would like to take up a few things in Bob's message. He says ... we are committed to the existence of a language given by a formal definition (........ ) This does not mean, however, that the language is nothing more than its formal definition. .... I'm not aware that anyone has put forward the latter strange view, so it's irrelevant and confusing to mention it. He also says To pretend that any modification to Standard ML creates a new and independent language flies in the face of reality. No-one pretends this, at least I don't. Languages evolve into each other. He says: Moreover, as Robin aptly points out, the revision of the definition in 1997 increased his (and my) confidence in it, not the other way around. In fact, in my message I explicitly asserted the other way around. I said "The result wasn't perfect; I trust the '97 Definition more in some respects, but less in other respects, than the '90 semantics." Finally he asserts Evolving the definition is no more difficult than evolving an implementation. Of course one can evolve a definition by simply deciding to change a few things, but this is clearly not what any of us would mean by evolving a definition. We would mean something much more careful, including coordinating it with implementations, checking self-consistency when changes permeate the semantics, and even ensuring that theorems which were proved (sometimes by semi-automatic proof systems) of the old definition remained true of the new. I'm not aware that this kind of comprehensive evolution of a fully formal definition of an industrial-strength language has ever been done; as I said in my message, I believe it's an open problem how to define languages in a way that supports change. To summarise: I haven't changed my view. I think it very reasonable that a group of people including implementers should put forward a proposed modification to Standard ML, under another name. The more who agree to take part the greater the likelihood of divergence, but the stronger the consensus when achieved. The community at large can then assess what has been done. I remain resolutely opposed to carrying out this exercise under the name Standard ML; I trust that using another name won't deter those who want to do the work for scientific reasons. I have held this view for a long time, and already taken too much space expressing it, so I probably won't send another message; but I hope the people on this list will take my view seriously into account. With regards Robin Milner |