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

[Zooko Wilcox-OHearn]

(N.B., the following doesn't really have almost anything to do with
Tahoe-LAFS, other than that Daira and Zooko are the two primary
maintainers of Tahoe-LAFS.)

.. -*- coding: utf-8-with-signature-unix; fill-column: 73; -*-
.. -*- indent-tabs-mode: nil -*-

LAFS Twice-Weekly Hack, 2014-04-17
==================================

Thursdays are always Tesla Coils and Corpses from now on. If you want to
attend on Thursdays, please contact Zooko to sign up. The topic for next week
will be either Noether, ZeroCoin, or a crypto idea for
no-added-round-trips-transitive-directory-lookup. (Which is a kind of
"encrypted search".)

Mondays are always Nuts and Bolts, likewise, please let Zooko know you want
to join Nuts and Bolts!


in attendance: Zooko (scribe), Daira


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

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.

possible next Tesla Coils and Corpses: Noether, ZeroCoin,
constant-time (no extra server-round-trips) directory-lookup


-- 
Regards,

Zooko Wilcox-O'Hearn

Founder, CEO, and Customer Support Rep
https://LeastAuthority.com
Freedom matters.