Hi, I use your notation with ==1 for distinguish different contract wrappers of same function or in my case object target and ==2 for considering different contract wrappers of the same function or in my case object target to be identical.
We use JavaScript proxies for implementing access permission contracts, which use a set of permitted access pathes to restrict effects. Our actual approach to get the ==2 is to make the proxy "transparent" and compare the target and not the proxy. Therefore we implement an handler trap, which is like a property of the proxy for saying compare with ==1 (if not exists or return false) or ==2 (if exists and return true). See: http://proglang.informatik.uni-freiburg.de/projects/JSProxy/proxy.pdf Best regards Andreas Am 30.12.2013 00:54, schrieb Cormac Flanagan: > 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 > <mailto: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 > <http://users.soe.ucsc.edu/%7Ecormac/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
