so first of all thanks to italic and
glad for asking me to come and it's it's
great to be here I'm glad glad to be
able to deliver a few impressions I
think in in twenty five minutes that's
all I can do is is deliver a few
impressions of ladin I've been working a
lot on Casper and and kind of the
technologies and tools and ideas that
I'm bringing to the formal verification
of Casper are also embodied and in some
of the ideas that I'll be presenting
here so kind of the you know just want
to touch on the an overall narrative and
then and really if you if you walk away
with nothing else I want to leave you
with this one big picture idea but but
you know in the details there's enough
space for God and the devil right so
there's always lots and lots of space
and in the details and and maybe talk
about some next steps so that's kind of
what we're going to do and the narrative
is actually a fairly simple one it's
fairly straightforward consensus is a
necessary component of the blockchain
so you heard Vlad talk rather eloquently
about consensus and some of the problems
there it turns out I mean I think I
think many of the people here know that
that blockchain currently you know as
embodied doesn't doesn't scale very well
and Casper's variation the proof of
stake is an important step along the way
towards scaling I wouldn't say that it's
it's the solution to scaling but it's
it's one component of a scaling solution
and so so we want to look at proof of
stake and in particular the the Casper
variant of proof of stake and really
bash on it from from the point of view
of a formal verification we'd like to
know for sure once and for all whether
Casper enjoys certain properties
and so we're one of the tools that were
using to go about this is something
called the applied PI calculus and this
gives us and I'll show kind of where we
are and in the state of that later in
the talk
but this gives us access to automated
support for a proof of correctness so
the tools that we're employing right now
in include Provera f-- but but much more
the spatial logic model checker which
was developed by lewis Scotties and that
turns out to be good fun and if you want
to look at the code it's up on github
and i'll give you a link of it in a bit
later but it turns out that if you have
a speck in the applied PI calculus well
I have a bunch of libraries that up on
github called Special K and they are an
implementation an executable distributed
virtual machine of the applied PI
calculus so if you have a spec you can
turn it straight into an implementation
so if you have a spec that you can
reason about the correctness properties
then you can actually run Casper and so
this this is has big implications for
the correctness of an implementation
what you get is correct by construction
and that's that's a that's a different
approach to design than I think you know
happens in a lot of software a lot of
the software industry but it but in
particular in this space I'm not sure
that that that the blockchain as
originally conceived was was done in a
correct by construction style and I
think it was quite quite the opposite
actually but but if you didn't take on
correct by construction one this helps
with scaling there are a lot of
different aspects to scaling right it's
not just about volume and performance
right it's also about when you have
reliability reliability is what
engenders adoption right so you think
about your yours your you're someone who
manages a large financial firm and
there's this great new technology that
promises wonderful things but am I going
to swap it out for the thing
it works well I might be more inclined
to do that take take on some of that
risk if I knew that it had certain
reliability properties that were
formally and automatically verified it
also helps with with maintenance and
evolution because as we know this space
is changing very fast and so it's kind
of important to be able to to adapt the
code to the needs of the space so it
turns out that in addition to some of
these benefits Special K provide already
of its own provides a broad range of
transactional semantics and and we get
these because of the monadic
decomposition of the the elements that
are that are used to to make these kinds
of transactions and I'll go through
those but you know there's there's
basically a handful of programming
paradigms that are used successfully
today in building distributed systems
and and it turns out that you can
organize all of those under a single
rubric under essentially a single API
additionally the compositional nature of
the the PI calculus so I'm just giving
you some sense of all the benefits of of
this kind of approach makes it possible
to write down in a single page a metered
distributed concurrent VM so just for
fun I'll show you that spec right at the
end ooh that's some nice feedback that's
some really nice high frequencies
okay so so the big picture is that
compositionality is the key to scaling
any system so if you forget every
everything else in this talk if you
remember that one idea you know I'm
hoping to plant that seed in your mind
and go home and think about that so what
the hell is compositionality is it even
a word right if spellcheck is gonna
underline it in red I guarantee you so
let me let me kind of unpack this idea
so so in computing I think we're all
familiar with the idea that scaling
refers to lots and lots of copies of
things that are you know potentially not
reliable individually right so lots of
chips lots of boxes lots of databases
lots of servers lots of data centers
right so that's the traditional you know
high-volume high-performance
notion of scaling compositionality turns
this upside down and what it says is
that scaling is about making the the
large reflect the small right and and
every child understands this idea they
hold up the leaf they look at the leaf
and they say hey there's a tree inside
this leaf right and that is in fact how
nature scales then we see it again and
again and again and it's kind of funny
why is it that we forget we knew this at
one point and then we forget it and why
is it that we forget this well it turns
out that it's actually a fairly new
thing for culture to remember this so
I'm just giving you a few examples from
pop culture of of this idea and you'll
notice that all of them I mean even
Mandelbrot sets are very new on culture
on the cultural landscape right and just
to give you another sense of how how
interesting and different this way of
thinking is so here's a bunch of people
who had computationally very effective
ideas right so you know maybe you know -
maybe you recognize Paul Dirac maybe you
recognize er
intro dinger but quantum mechanics as
formulated in those days was not
compositional and it's only been in the
last five years that we've had a
compositional formulation or
presentation of quantum mechanics via
Simpson of RAM ski-in Bob Kocher a
similar thing has happened in the
physics of the large gravitation and
cosmology and because we don't have good
compositional accounts physics fails to
scale we don't have a nice way to marry
those two ideas so if you're feeling
like hey I'm not quite sure what
compositionality is I'm not sure not
sure well these guys didn't either
so it's kind of okay but what I can say
is that the notion of composition has
has nice formalizations so in the since
about the 1950s there's been an
appropriately parametric notion of
composition that was formulated first in
category theory and it was given this
weird crazy name of a monad if you if
you pair monads with their dual
mathematical widget the comonad you
couldn't think of them so composition is
kind of like nesting right it's like the
Russian dolls you you nest you you know
it's like the the the the tree inside
the leaf and the leaf inside that tree
and the tree inside the leaf right so
it's about nesting and and what what
monads and Co monads give you monads
give you a way to zoom out and comb
monads give you a way to zoom in on this
nesting phenomena or this composing
phenomenon and lest you think I'm
talking about abstract airy-fairy stuff
again I'm sure all I can do in 25
minutes is give you a few impressions
right so so here are effective api's
expressed in the language Scala you can
find similar expressions in the language
Haskell just out of curiosity how many
people code in functional languages here
awesome how many people use monads in
their daily practice you know quite a
few less yeah okay
but but the point is that they are an
effective notion and they're a great way
to structure a code even if you're not
thinking about scaling blockchains
they're they're a great way to structure
container code they're a great rate of
constructor to structure control flow
but it turns out that that we can do
better than that
so in particular Special K kbdb
looks at a duality between continuation
which is the rest of your program so
let's say your program walks up to the
block tier and says I'm looking for
something right and what if that
something isn't there yet what do you do
with that program that is waiting for
data and can't go further right so in
Special K what happens is the rest of
that program is packaged up as a piece
of data and stored at the place where
you were it was looking for something
right so that's the continuation and
then data is dual to that and in fact
you can have a notion of data integrity
that that goes all the way back to the
law of excluded middle right a or not a
right that has to do with this duality
between continuation and data so at this
location that you're looking for this
address on the blockchain or in the case
of Special K it's a it's a more
sophisticated kind of key but if it's
location you will either have a
continuation or some data and if if a
program is looking for for data and it's
not there the continuation will be
stored there if a program is depositing
data if there is a continuation there
that continuation will be woken up and
handed the data okay that's the basic
set up right now you can ask some
questions about that set up you can say
well after the data and the program the
continuation meet each other what
happens and there are there are only a
handful of possibilities one is the data
disappears and the continuation
disappears so they meet each other in
this abstract space this this address
and they go poof all right another
possibility is that the continuation
remains and the data goes poof another
possibility is that the continuation
goes poof
the data remains and the last
possibility of course is that they they
both persist right so so what is what
does that have to do with traditional
approaches to distributed applications
well if it well if the data persists and
the continuation evaporates
that's just traditional deep database
operations think about a read/write my
program once the data I read it but I
don't get rid of it out of the database
just from the read operation right
that's that's traditional database
operations if I publish and and and the
the the publishing data is ephemeral but
the continuation persists that's
ordinary published and subscribed
that's ordinary publish and subscribing
if they if both of them persist its
published and subscribe with a history
with a backlog of what you published and
finally this is quite interesting if
they if they both disappear then you get
item level locking in a distributed
transactional semantics so one API which
I showed you nothing up my sleeves right
one API the the monadic api covers all
of those distributed programming
paradigms so now how does this apply to
the blockchain well that that that how
we provide that is that the continuation
monad is the is the monad underlying
being able to bring those those patterns
together right so we talked about this
duality between continuation and data
well it's the it's the structuring of
the continuations and the way we store
them that uses the continuation monad to
provide to provide that unification of
all those programming paradigms and and
so we looked at that API it turns out
that if you just tilt that API on its
side a little bit what you end up
getting is the applied PI calculus and
that's exactly how Special K
is organized so if you look at Special K
if you go to github right now and you
look at Special K what you'll find is a
little DSL that provides an
implementation of the applied PI
calculus so but here's a little preview
of applying that API to Casper so I
spent last night and refactored this I
had good fun so let's see if I can can
you see that well that's that's all
right so I'm just gonna again I only
have time to give you a flavor so here
are the files in the spec and let's take
a look briefly at just some of them so
in in Casper the consensus protocol is
organized around nodes which we think of
as validators and what a validator wants
to do is essentially receive blocks and
then make bets on whether or not a block
should be published to the to the to the
to the blockchain and here's here's
basically just an applied PI calculus
spec of the bedding and the the
convergence around bedding spec for the
validator we can
there are similar and you can see how
tiny it is it's it's teeny tiny this
this Wow we are already at two minutes
okay come see me afterwards and I'll
show you probing this spec for
properties okay so well I'll I'll cut to
the cut to the chase
so I was gonna give you a demo but I
would like to just take take a just come
to come see me afterwards and I'll give
you a lot more of the flavor of the spec
and how how we can probe it
automatically with the spatial logic
model checker but I would like to
conclude by just taking you through a
little bit taking these same kind of
specs and using the compositional
structure we can walk this structure we
can essentially build up a new semantics
from the existing semantics in a nice
clean careful way so I took the I took
the essentially a variant of the applied
PI calculus and I added to it metering
and this metering basically uses three
elements so there's a resource there's a
there's an a channel for the exchange of
the resource and there's a channel for
the next step that next step is again an
encoding of a continuation and what we
see here is essentially just just a tiny
little harness for for running a metered
VM we run inside that harness the
translation of our of our little tiny
API for for contracts right but this
this API and this contract language is a
little different and the reason it's
different is because contracts can be
executed in parallel contracts have have
other interesting properties in that
contracts themselves can be reified in
exchanged the important point here again
I'm happy to go through all the details
with you offline but the important point
here is the size of this spec and not
only the size of this spec but the
correctness properties of this virtual
machine can be stated and proved in
about 1/2 a page right so even more
interestingly you can take this kind of
virtual machine and bootstrap so you can
build this virtual machine on top of
this virtual machine and it would be
interesting to look at look at doing
that with the existing VM
that would be an interesting question
could we build the etherium blockchain
on top of the existing vm does it
bootstrap and that that that brings us
that to the point I was trying to make
at the very beginning do we have this
self loop right because that's your
first and best test that you can scale
so the big picture that I want to leave
you with is that is that
compositionality this this kind of
finding the small and the large the
large and the small is the key to
scaling any system so thank you