report from Tesla Coils and Corpses, 2014-04-17
daira at jacaranda.org
Sun Apr 20 13:37:35 UTC 2014
On 19/04/14 21:50, Zooko Wilcox-OHearn wrote:
> topic: Noether!
> Noether-C. Might already be a consistent logic. The main reason it is
> not is that it includes failure. Shouldn't be too hard to define it as
> a consistent logic except that it can fail. If Noether-C is, or can be
> made to be, a consistent logic, then it would be more convenient to
> use Noether-C as a proof-system for Noether code than it is to use
> Agda as a proof-system for Haskell code.
> *All* function calls are atomic in Noether (all side-effects are
> rolled back if the function raises an exception).
> This is related to Software Transactional Memory, although STM is more
> for concurrency than for error-handling.
> E-like separation between immediate and eventual send (function call).
> … plus Erlang-style blocking-receive
> Zooko: When do you want to use blocking-receive for anything *other*
> than to implement an E-like event loop and then never see
> blocking-receive again?
> Daira: to implement things like: try a turn, if it fails then repeat
> it but with logging turned up to the max
> difference between yield and blocking-receive
> Zooko was concerned that this could "yank the rug out from under" the
> programmmer if they were reasoning about the runtime state, while
> looking at the code, and then at runtime a blocking-receive ends up
> letting unpredictable *other* code run which alters the runtime state.
I also explained that this should not be a problem for several complementary
* the ability to do a blocking receive of the next message sent to a vat
requires a capability to an outlet of the vat's mailbox;
* blocking is an effect that is tracked by the effect system;
* it's possible to declare that none of the code executing *within*
a turn has the blocking effect.
That is, to block you need *both* a mailbox outlet capability, and to have
a declared effect that includes blocking. When you construct a vat, you
declare the effect that turns must be constrained by, so enforcement of
E's concurrency model is expressible as a special case.
[In Noether vats are not a primitive construct, they are a library
abstraction. The underlying concurrency model is pure actors with
channels, like in Joule. Mailboxes are implemented as channels, and an
"outlet" is an end of a channel that you can read from.]
> See MarkM's and Glyph's rants on the topic:
Thanks! I'd read the first of these but not the second.
> Parties (both "Nuts and Bolts" parties and "Tesla Coils and Corpses"
> parties) should be 1.5 hours instead of 1.0 hours. Daira and Zooko
> never want to stop after just 1 hour!
> Rust's disjoint heaps, borrowed-pointers and unique pointers
> In Rust, the idea of having unique heaps was the motivation of having
> unique pointers and borrowed-pointers. In Noether there is a different
> motivation: you can use it to separate the language into more layers.
> You can do things that look like mutating state within the
> pure-functional subsets. There's another language that does this:
Another example of this is that unique references are useful to enforce
deterministic use of channels.
Daira Hopwood ⚥
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 555 bytes
Desc: OpenPGP digital signature
More information about the tahoe-dev