> Hmm. I thought the motivation for using SML is that it had a definite > formal semantics (for which the last revision was published a decade ago),
Not really; I suppose it's nice to know that the underlying meta-language is formalized, but this would really only provide practical utility if we were proving theorems about ES. While there are interesting theorems that you might like to prove, it's not as high a priority as the actual design, specification, and reference implementation work. Being able to execute the spec and run test cases is an enormous leap forward in terms of quality assurance; being able to prove correctness properties would be even better but not as *much* better as just being able to run code. In practice, proving theorems about PL's means either choosing stylized subsets or using mechanized frameworks. It's just not efficient or cost-effective to prove theorems manually about artifacts as large as real-world languages. Mechanized frameworks like ACL2, Coq, Twelf, and Agda are making great progress, but they are still unwieldy and too challenging. We settled on ML as a simple, well-understood language that is well-suited for implementing PL's. Down the road, if we were to use one of these mechanized frameworks, we'd have to transliterate the RI code into the meta-language of the framework we'd chosen, which would be stylistically similar to ML but wouldn't be ML. And the language wouldn't have *any* of the side effects of ML, so then we'd still have to add shift/reset on top of the meta-language, as well as mutation and exceptions (and possibly even non-termination). > that had already been looked at and understood by many people. > Handwaving about the possibility of adding delimited continuations to > that formalization is not the same thing, even if you are right in > saying it is "easy". I've written a paper that shows you can implement shift/reset in ML as a library using call/cc [1]. And call/cc is very well-understood -- it's been around for decades in Scheme and has been formalized repeatedly, and it's been in SML/NJ for over a decade. It's been added to models of ML in the literature and proved type-sound. More directly, shift/reset has been formalized as well. But that's for the academic pin-heads. :) In much more conceptually appealing terms, this is my favorite explanation to date of delimited continuations: http://blog.moertel.com/articles/2008/05/05/olegs-great-way-of-explaining-delimited-continuations I like to imagine that demonstrates that as programmers we actually already have good intuitions about delimited continuations, and that they aren't as scary as they sound. But you're right that this comes down to a question of clarity. Which option is more obfuscated: specifying the entire language in CPS just for one feature, or using an esoteric low-level language construct that isn't well-known outside of the research world? It's definitely a trade-off. But I don't think the real concern is whether this makes the spec "less formal." It's just a concern about clarity. Dave [1] http://www.ccs.neu.edu/home/dherman/research/papers/icfp07-great-escape.pdf _______________________________________________ Es-discuss mailing list Es-discuss@mozilla.org https://mail.mozilla.org/listinfo/es-discuss
