report from Tesla Coils and Corpses, 2014-04-17
zooko at leastauthority.com
Sat Apr 19 20:50:23 UTC 2014
(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
Mondays are always Nuts and Bolts, likewise, please let Zooko know you want
to join Nuts and Bolts!
in attendance: Zooko (scribe), Daira
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
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:
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:
possible next Tesla Coils and Corpses: Noether, ZeroCoin,
constant-time (no extra server-round-trips) directory-lookup
Founder, CEO, and Customer Support Rep
More information about the tahoe-dev