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 <[email protected]>wrote:
> On Mon, Jan 14, 2013 at 6:30 PM, Mark S. Miller <[email protected]>
> 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
> [email protected]
> https://mail.mozilla.org/listinfo/es-discuss
>
_______________________________________________
es-discuss mailing list
[email protected]
https://mail.mozilla.org/listinfo/es-discuss