New paper: "Distributed Electronic Rights in JavaScript"

Cormac Flanagan cormac at cs.ucsc.edu
Tue Jan 15 09:11:16 PST 2013


Perhaps one useful aspect to add to this discussion is the distinction
between

* contracts as implemented as a DSL (as in Racket)

* contracts (aka attenuators/...) implemented as code

Both achieve the same functionality of constraining behavior.
Contracts-as-code may be more flexible but may have more ability to change
(rather than just constrain) behavior, whereas contracts-as-DSL gives
simpler contracts, perhaps better blame, and may be easier to reason about.

I am inclined to view them as alternate ways of expressioning the same
ideas.

      - Cormac


On Mon, Jan 14, 2013 at 3:47 PM, Sam Tobin-Hochstadt <samth at ccs.neu.edu>wrote:

> On Mon, Jan 14, 2013 at 6:30 PM, Mark S. Miller <erights at google.com>
> wrote:
> >
> > The footnote I (again, perhaps unwisely) deleted is:
> >
> >> Although types as contracts [2] and higher order contracts [3] can be
> seen as very
> >> special cases of smart contracts, their purpose is typically different:
> locating bugs
> >> during development rather than protection from misbehavior in the wild.
> >
> >> 2. Meyer, B.: Applying Design by Contract". IEEE Computer 25(10) (1992)
> 40{51
> >> 3. Findler, R.B., Felleisen, M.: Contracts for higher-order functions.
> ACM SIGPLAN
> >>     Notices 37(9) (2002) 48--59
>
> I think there are two fundamental mis-understandings of the work on
> behavioral contracts here.  First, that they're mostly about types and
> type-like properties.  On the contrary, contracts are useful precisely
> because they express far more than conventional types.  Matthias
> Felleisen suggests the following example:
>
> >    (add-edge
> >     ;; adding an edge (from,to) with cost w to this graph
> >     (->dm ((from node?)
> >            (cost (and/c real? (cost/c (get-field low-cost this)
> (get-field high-cost this))))
> >            (to   node?))
> >           #:pre (triangle-condition-preserved (send this edges) from
> cost to)
> >           any))
>
> which enforces that the triangle inequality is preserved on
> edge-insertion into a weighted graph.
>
> Second, that they're mostly about development and not production.
> Behavioral contracts are no more about development-only than array
> bounds checks are.  It's an unfortunate fact of modern software
> development that both are often omitted in production systems, to the
> detriment of users as well as developers, but contracts are a
> fundamental way of finding errors and allocating responsibility for
> them in both production and development.
>
> Sam
> _______________________________________________
> es-discuss mailing list
> es-discuss at mozilla.org
> https://mail.mozilla.org/listinfo/es-discuss
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.mozilla.org/pipermail/es-discuss/attachments/20130115/3dd0e777/attachment.html>


More information about the es-discuss mailing list