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
* 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
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>
> > The footnote I (again, perhaps unwisely) deleted is:
> >> Although types as contracts  and higher order contracts  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)
> >> 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.
> es-discuss mailing list
> es-discuss at mozilla.org
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the es-discuss