Richard Uhtenwoldt wrote:
Now a request: can someone please post or send me sample code
that _uses_ a deeply-immutable function? The object-oriented
nature of E code makes it less than ideal for my purpose because
hard to translate into Haskell, so I'd prefer pseudo-Scheme or
pseudo-BitC code.
Here's the *-properties example from p16 of
<http://www.erights.org/talks/asian03/paradigm-revised.pdf> translated into
pseudo-Scheme with bitc-style type declarations. For the present discussion,
the issue isn't the *-properties, but the confinement that it's built on.
I renamed the ":Factory" guard to ":deep-frozen" to emphasize that Cassie's
assurance -- that the calculators she makes are confined -- depends only on
the calc-factory being deeply immutable. I likewise changed the ":int"
declaration of write's val parameter to be ":deep-frozen", since that captures
the relevant property of ":int" that Cassie depends on to prevent Boebert's
attack.
(define (accept-product (calc-factory :deep-frozen))
(let (diode 0) ; in pseudo-bitc you'd declare diode to be mutable
(define (diode-write (val :deep-frozen)) (setq diode val))
(define (diode-read) (diode))
(define q (calc-factory ... diode-write ...))
(define bond (calc-factory ... diode-read ...))
...))
"..." above does not represent a Scheme token but rather just other code that
we assume is not relevant to this example, matching the "..."s in the
original example.
Even if one is not interested in language level security per se, this ability
to reason about limits on the influence of side effects is quite valuable. Of
course, Monads also enable one to reason about limits on the influence of side
effects. It would be interesting to explore how the kinds of limits enabled by
each of these techniques relates to each other.
--
Text by me above is hereby placed in the public domain
Cheers,
--MarkM
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
