report from Tesla Coils and Corpses, 2014-04-17

[Daira Hopwood]

On 19/04/14 21:50, Zooko Wilcox-OHearn wrote:
> topic: Noether!
> 
> https://github.com/daira/noether/blob/master/doc/presentations/StrangeLoop/noetherj.pdf?raw=true
> 
> 
> 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
reasons:
 * 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:
> 
> http://www.eros-os.org/pipermail/e-lang/2001-July/005418.html
> 
> https://glyph.twistedmatrix.com/2014/02/unyielding.html

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:
> Clean.

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...
Name: signature.asc
Type: application/pgp-signature
Size: 555 bytes
Desc: OpenPGP digital signature
URL: <http://tahoe-lafs.org/pipermail/tahoe-dev/attachments/20140420/4002aa51/attachment.pgp>