Hi Mark and everybody, That is quite a long thread to digest all at once, but very interesting!
Certainly, the API of our Temporal Contracts paper provides a way to enforce non-interference (aka projection) by allowing user-defined code to observe all behaviors of a function, and to fail on erroneous behavior (but not otherwise influence program execution, except perhaps by diverging). We formalized it only for a small calculus (the imperative by-value lambda calculus), and scaling it to a realistic language would need to address some additional issues. In particular, our paper calculus does not deal with EQ at all. As the thread discusses, equality is a total pain for trying to have contracts be projections. It seems there are two relevant notions of observable equivalence here: - the traditional notion, perhaps denoted \obseqv_1 - and observable equivalence modulo failure, \obseqv_2, so two terms are considered equivalent even if one sometimes fails a contract that is absent in the other. Clearly obseqv_1 => obseqv_2, but likely not vice-versa. I expect that adding contracts does not preserve \obseqv_1, but perhaps does preserve \obseqv_2, provided that the contracts are non-interfering (aka projections). There are two corresponding notions of equality we could define. ==1, which under-approximates \obseqv_1, and distinguishes different contract wrappers around the same function. ==2, which under-approximates \obseqv_2, and considers different contract wrapping of the same function to be identical. If we use ==1, then standard transformations discussed in the thread preserve \obseqv_1. If we instead use ==2, then some of those transformation actually break \obseqv_1, and instead only preserve \obseqv_2. Moreover, if the language includes ==1, then \obseqv_2 is perhaps not that much bigger than \obseqv_1, since a contract on a function is now observable, and so adding contracts (even a well-behaving contract like Int->Int) likely now breaks \obseqv_2. Of course, once we add failure catching exception handlers, the whole notion of \obseqv_2 and ==2 perhaps makes less sense, and maybe \obseqv_2 even collapses to \obseqv_1. So an interesting question is what is the right projection-like correctness property for contracts in a language with EQ and exception handlers that can catch failures. One (perhaps simplistic) approach is to prove the projection property only for programs that do not use those features. I hope this makes some sense. I am still trying to internalize the whole thread. Best, - Cormac On Fri, Dec 27, 2013 at 3:14 PM, Mark Miller <erig...@gmail.com> wrote: > [+tdisney, +cormac] > > On Fri, Dec 27, 2013 at 4:47 AM, Philip Wadler > <wad...@inf.ed.ac.uk<https://mail.google.com/mail/?view=cm&fs=1&tf=1&to=wad...@inf.ed.ac.uk> > > wrote: > >> This thread has gone dead. I am excited at the prospect that JavaScript >> might support proxies for contracts if a suitably expressive 'sublanguage >> of projections' can be isolated. Is there any progress? How can I help >> carry this forward? Yours, -- P >> >> >> . \ Philip Wadler, Professor of Theoretical Computer Science >> . /\ School of Informatics, University of Edinburgh >> . / \ http://homepages.inf.ed.ac.uk/wadler/ >> >> The University of Edinburgh is a charitable body, registered in >> Scotland, with registration number SC005336. >> > > > The more I think about it, the more I think the work on Temporal Contracts > <http://users.soe.ucsc.edu/~cormac/papers/icfp11.pdf> by Tim and Cormac > (cc'ed) is relevant. > > Tim and Cormac, our normal notion of a contract is that it should be a > projection, i.e., that the contract may only cause rejection or > non-termination but may not otherwise change the observable behavior of the > system to which they are added. However, the other contract frameworks > we've discussed so far on this thread are not able to enforce that the > contracts that parameterize the framework may only be projections. IIUC, > because your contracts are predicates on event sequences, the contract > framework need only provide the contracts with information about the > computation, and need not ever provide direct access to the mutable objects > engaging in the computation of interest. The contracts need only be > provided with these event sequences as input, and need only be provided > with the ability to signal acceptance or rejection as an output channel. > Given a system that can enforce confinement, the contracts need not be > given any further access to the world outside themselves. > > If all this is true. then this becomes a meaningful context in which to > explore the object identity issues of the title. I'll separately forward > you the messages of this thread to date for background. > > > -- > Cheers, > --MarkM > _______________________________________________ dev-tech-js-engine-internals mailing list dev-tech-js-engine-internals@lists.mozilla.org https://lists.mozilla.org/listinfo/dev-tech-js-engine-internals
