[racket-dev] RFC: "provide" via mutation

The following program implicitly does something like `provide', via mutation.

#lang racket/load

(module store racket
  (define s (box #f))
  (provide s))

(module m typed/racket
  (require (for-syntax 'store))
  (define: (x) : Number 1)
  (begin-for-syntax (set-box! s #'x)))

(module n typed/racket
  (require (for-syntax 'store) 'm)
  (define-syntax (mac stx)
    (define myx (unbox s))
    #`(add1 (#,myx)))
  (mac))

(require 'n)

The certificate system currently allows this, although it's not
obvious to me that it should.  Typed Scheme also ensures that it
typechecks.  However, Typed Scheme could save a bunch of work at
startup if this didn't have to typecheck.  What do people think is the
right tradeoff?  Does anyone care about programs like this?  Should
the certificate system allow them?  Should Typed Scheme make them
work, at the cost of some performance?
-- 
sam th
samth at ccs.neu.edu