You have gotten plenty of good answers so let me focus on some of the 
high-level points and some details that people didn’t respond to: 

> On May 2, 2017, at 6:01 PM, Daniel Prager <> wrote:
> More concise and clear expression of contracts
>       • The implies operator

Missing but I am sure we would accept a pull request on that one. 

>       • Proper support for invariant-checking

Well. It’s kind of there (see appended code at end) but not exactly. Eiffel has 
re-entry problems with invariants and Spec# cleaned this up a bit. We have a 
‘boundary philosophy’ (see beginning of Contract Guide and what I wrote there) 
and that is much cleaner but distinct from Eiffel for sure. 

>       • Proper support for covariant inheritance

That’s unsound so we did not want to go there. 

>       • Tools for automatically generating documentation

Good idea. We have bits and pieces for that. Nothing too useful. 

>       • Better tools for turning off contracts by configuration

As Tony Hoare said, what do you think of a boater who practices on land with 
his swim vest on and then goes to sea and takes the swim vest off? 

> My questions are: 
>       • Is it feasible to get similar behaviour from the official contract 
> system?, or
>       • Do these considerations call for building up an alternative system?

Yes you can. Racket’s contract system is far more expressive than Eiffel’s. It 
also repairs obvious short-comings (a polite way of saying problems) with 

What you are missing is what you can do with macros. 

> Restating my goals:
>       • Specify pre-conditions and post-conditions as simple predicates 
> (boolean expressions)
>       • Selectively turn off contracts (mainly post-conditions) for 
> performance in well-tested code.

See Hoare above. See Macro above. See the Literature pointer in Ben’s message. 
We want you to take responsibility for taking the swim vest off. 

#lang racket

(module server racket
    (c% (class/c (field [x positive?]) (setter (->m number? number?))))))

  (define c%
    (class object%
      (field [x -1])
      (define/public (setter x*) (begin0 x (set! x x*))))))

(module client racket
  (require (submod ".." server))
  (define c (new c%))
  (displayln `(the initial value does not have to live up to the field contract 
,(send c setter 2)))
  (with-handlers ([exn:fail:contract? (lambda (xn) (displayln `(you can't get 
away with bad sets)))])
    (send c setter 0)))

(require 'client)

You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
For more options, visit

Reply via email to