►
Description
Agoric's Chief Scientist talks about creating an object-capability (ocap) secure subset of JavaScript to support simple composition with least authority.
Agoric enables application developers to write safe smart contracts and empowers individuals to securely execute transactions, establish new markets, and craft novel patterns of exchange — without centralized control.
ABOUT
Build Fast, Earn Fast - Agoric enables developers to rapidly deploy dapps and DeFi markets on-chain using composable JavaScript smart contracts. Safely get your project from vision to global market.
LINKS
https://agoric.com
https://agoric.com/twitter
https://agoric.com/discord
https://agoric.com/telegram
https://agoric.com/newsletter
Click the 'SUBSCRIBE' button to follow our Youtube channel!
A
I'm
going
to
take
you
up
several
levels
of
abstraction.
The
first
one
is
machines,
we're
all
building
on
top
of
computers.
Each
of
these
individual
planes
is
a
physical
machine,
but
the
stacking
indicates
something
else.
From
our
perspective,
a
blockchain
is
really
just
a
logical
machine.
It's
a
machine.
That's
built
out
of
agreement
between
a
massive
number
of
physical
machines,
but,
logically,
in
terms
of
programming
it
we
see
it
as
a
machine.
The
solo
machine
is
actually
just
a
physical
machine.
A
Is
it's
conventional
and
then
the
core
machines
are
where
you
have
moderate
replication
still
to
give
rise
to
a
logical
machine.
Those
would
be
like
permission
or
mechanisms
like
hyper
ledger,
so
what
we
want
to
do
is
build
a
level
of
abstraction
across
all
of
these.
We
want
to
treat
each
of
these
machines,
whether
the
solo
machines,
horns
or
chains
as
nodes
in
a
cryptographic
distributed
system,
so
we're
building
a
cryptographic
protocol
by
which
these
things
can
communicate
with
each
other.
A
A
Subset
of
JavaScript
I've
been
on
the
committee
now
the
Ekman
script
committee
for
10
years,
helping
fashion
JavaScript
into
a
language
that
can
support
this
and
then.
Finally,
on
top
of
that,
we
have
our
actual
smart
contract
layer
by
building
up
to
first
having
a
clean
layer
of
secure
distributed
objects.
We
now
have
a
basis
for
building
electronic,
writes
and
smart
contracts
in
a
much
simpler
and
more
confident
manner
and
in
a
manner
that
can
be
made
accessible
to
too
many
more
non
expert.
A
Programmers
and,
what's
particularly
interesting,
I,
want
to
call
your
attention
to
these
smart
contracts
and
Ear
I'ts
in
a
loop
over
there.
You
rights
are
electronic
rights.
Smart
contracts,
manipulate
rights,
but
smart
contracts
in
manipulating
rights
themselves
create
new
rights
and
the
new
rights
that
they
that
they
create
can,
in
turn
be
manipulated
by
smart
contracts.
A
A
That
TP
is
the
protocol
that
builds
the
that
level
of
abstraction
out
of
the
machine
level
of
abstraction
cap
TP
for
a
capability
transport
protocol
builds
the
Oh
cap
level
of
abstraction
out
of
the
VAT
level
of
abstraction
and
then
er
TP.
The
electronic
rights
Transfer
Protocol
build
the
rights
and
contracting
level
of
abstraction
out
of
the
object
level
of
abstraction.
A
A
So
the
basic
step
of
object-oriented
programming
is
when
object.
Alice
says,
for
example,
Bob
dot,
foo
of
Carol,
invoking
the
Bob's
foo
method
with
Carol
as
an
argument,
so
these
within
arrows
represent
object.
References
and,
what's
showing
here,
is
that,
if
object,
Alice
already
has
a
reference
to
Bob
and
already
has
a
reference
to
Carol,
then
Alice
can
invoke
Bob
with
that
reference.
The
thing
that
makes
that
to
get
from
object
to
object
capabilities,
we
only
need
to
impose
some
restrictions
that
are
very
natural
restrictions.
A
From
the
point
of
view
of
the
object
programmer
that
these
references
that
carry
messages
that
those
references
are
the
only
thing
that
carries
causality,
so
one
object
can
affect
another
only
by
invoking
its
public
interface
and
an
object
can
only
affect
the
world
outside
of
itself,
according
to
the
references
that
it
holds
and
the
references
it
holds
as
we
see
here
can
also
pass.
So
the
result
is
that
references
are
the
only
representation
of
permission.
A
But
this
dot
here
creates
a
problem.
This
dot
is
the
is,
is
the
immediate,
controlled
return
control
flow
where
Ellis
is
invoking
Bob
right
now?
Does
a
control
transfer
to
Bob,
but
Bob
executes
Stu
completion
returns
to
Alice
and
everything
that
Bob
does
while
it's
invoked
is
part
of
Alice's
transaction
and
because
Alice
is
suspended,
bob
could
call
back
into
alice,
even
though
alice
might
be
juggling
a
bunch
of
state
is
in
a
delicate
situation,
but
bob
calling
back
into
alice
in
that
situation
creates
reentrant
c
hazards
such
as
the
DAO
bunt
was
an.
A
It
was
an
example
of
that
kind
of
synchronous
call
back
while
a
caller
had
various
state
in
the
air.
So
this
kind
of
synchronous
interaction
is
only
appropriate
locally,
only
appropriate
if
Alice
and
Bob
are
co-located.
In
the
same
that
we
introduced
this
in
fixed
bank
operator.
The
eventual
send
operator
that
does
an
asynchronous
invocation
sends
the
message
foo
to
Bob,
eventually
to
be
delivered
to
Bob
in
a
separate
transaction
and
when
Alice
sends
that
sends
that
message
off.
A
The
message
send
immediately
returns
to
to
Alice
a
promise
for
what
the
result
will
be
and
now
Alice
and
Bob
are
protected
from
each
other.
Alice's
transaction
completes
without
being
affected
at
all
by
Bob's
activities
in
reaction
to
the
message,
and
likewise
when
Bob
receives
the
message
that
starts
a
new
transactions,
they
have
nice
temporal
isolation,
keeping
them
from
disrupting
each
other.
So
now
Bob
can
be
local
or
remote.
Alice
doesn't
have
to
care.
Where
Bob
is
it's
the
same
programming
paradigm.
B
B
A
It's
it's
a
it's
a
an
object
that
we
refer
to
as
a
promise
that
designates
that
that
is
used
to
designate
what
the
value
will
be
at
some
future
time
when
the
value
is
determined
that
object
the
promise.
Actually,
that
does
designate
the
value
at
that
time.
The
cool
thing
about
a
promise
is
the
same:
eventual
send
can
be
done
on
the
promise.
A
So
if
you,
if
Alice,
if,
if,
for
example
in
this
example
of
Bob
here,
is
itself
a
promise
for
the
result
of
a
previous
operation,
then
the
foo
message
actually
gets
queued
in
the
promise
waiting
for
the
promise
to
get
resolved,
and
once
the
promise
is
resolved,
it
then
gets
forwarded
further
to
the
resolution.
So,
as
you
as
you
do,
eventual
sends
you
get
promises
on
which
you
can
do
further
eventual
sentences
and
the
promise
abstraction
we're
using
here
is.
A
Great
question:
the
question
is:
how
do
you
know
you
got
a
result
back
so
there's
essentially
two
fundamental
operations.
You
can
do
with
the
promise.
You
can
do
this
eventual
send,
which
just
pushes
new
things
in
doesn't
lever.
Tell
you
what
you
got
back
and
then
there's
another
operation
that
there
will
be
an
example
of
later.
It's
not
an
example.
I
emphasize
I'll,
just
tell
you
about
it
right
now.
There's
a
operation
called
then
so
you
you
give
you
say
to
a
promise
dot
then,
and
then
you
give
to
call
back
arguments.
A
One
call
back
is
the
success
callback
and
the
other
is
the
failure
call
back.
So
if
Bob,
when
he
receives
this
message,
if
his
transaction
aborts
with
an
error,
then
the
promise
of
the
result
becomes
a
rejected
promise.
If
the
operation
returns
a
value,
let's
say
the
number
eight,
then
the
promise
becomes
fulfilled
with
eight.
If
you
do
a
dot,
then
I
want
to
promise
with
the
two
callbacks
that
it
gets
fulfilled
with
eight.
Then
the
success
callback
gets
invoked
with
eight.
B
A
A
So
here
Alice
still
think
she
has
a
reference
to
Bob.
The
each
VAT
is
now
divided
into
two
portions.
Local
SES
SES
is
secure,
Agnes
crypt,
it's
the
object
capability,
subset
of
JavaScript
that
we've
created
and
then
cap
TP
surrounds
that
that's
the
serialization
on
serialization
layer,
all
of
the
application,
the
normal
application
programmer.
All
of
the
objects
that
normally
concerned
with
are
just
the
ones
that
live
inside
the
respective
SES
boxes.
All
of
the
rest
of
this
is
just
the
infrastructure
that
makes
it
work,
so
their
messages
can
get
from
one
object.
A
A
Which
I'll
explain
in
a
moment,
but
first
the
export
tables
computation
a
block
chain,
cannot
keep
secrets.
So
we
had
to
reformulate
a
lot
of
how
we're
doing
things
so
that
all
of
the
access
control
all
of
the
distributed
security
could
work
without,
depending
on
transmitted
secrets
and
without
without
having
the
object.
Computation
at
the
endpoints
internally
have
to
have
secrets
so
be
so
Bob
being
entered
into
the
export
table
that
that
that
a
can
use
when
a
message
comes
in
to
that
B.
A
From
that
a
the
fact
that
it's
authenticated
as
being
from
that
a
is
the
thing
that
lets
that
B
know
that
it
that
that
that
that
message
can
address
that
table.
So
the
index
in
that
table,
which
is
Mac
between
a
and
B,
is
how
that
a
talks
to
that
B
about
Bob
that
C
can't
currently
access
Bob,
because
Bob
is
not
exported
through
the
export
cable.
Does
that
C
can
access.
A
And
then
the
handoff
tables
have
have
a
particularly
restrictive
rule,
which
is
that
sees
hand
off
table
from
A
to
B
is
one
where
only
that
a
can
instruct
that
C
as
to
what
to
place
into
the
table,
and
only
that
B
can
instruct
that
C
as
to
what
to
take
out
of
that
table.
That's
the
A
to
B
table
on
on
the
left.
A
So,
when
Alice
sends
that
message
to
Bob
what
she's
really
doing
that
the
object
level
is
sending
it
to
a
local
proxy
for
Bob
that
has
to
serialize
the
message.
The
first
step
of
that
serialization
is
that
that
a
sense
to
that
be
a
give
to
message
saying
that
a
is
essentially
saying
to
that
see
when
that
B
asks
you
for
an
index
that
Carol
A
to
B
is
just
an
index
that
that
a
made
up
when
that
B
asks
you
for
that.
A
A
That
beacon
contain
complete
unsee,
realizing
the
message
into
an
object
message
which
it
then
delivers
to
Bob
and
now
Bob
has
the
promise
for
the
result.
Bob
can
continue
computing,
even
though
none
of
these
messages
for
VAT
C
have
actually
reached
VAT.
Seeing
that
C,
in
fact
could
be
off
lined
with
all
these
messages
just
accumulating
in
some
store
and
forward
infrastructure
somewhere.
A
Now,
in
our
crypto
world,
of
course,
a
crypto
multi
machine
world
there's
a
lot
more
going
on
than
just
serialization
on
serialization.
There's
also
create
encryption
and
decryption
and
signing
and
signature
verification
and
a
whole
routing
fabric
standing
between
these
machines
to
get
messages
from
one
to
the
other.
A
And
the
overall
flow
is
that,
when
Alice
sends
an
object
message,
it
lands
in
cap
TP
that
has
to
serialize.
It
delivers
it
as
a
serialized
blob
to
that
TP
that
encrypts
it
sends
it
over
the
network
to
the
other
sides
of
a
TP
that
decrypt
it
into
a
binary
blob.
That
needs
to
be
unsee
realized
into
an
object
message
and
delivered
to
Bob.
Now.
A
A
A
A
So
the
network
partition
so
the
so,
if
there's
a
network
partition,
then
the
side
of
the
partition
in
which
there
are
participants,
if
any
in
which
there
are
participants
that
are
able
to
meet
the
threshold
on
that
side
of
the
partition,
the
VAT
can
continue
to
move
forward
and
other
things
on
that
side
of
the
partition
can
see
it
outside
the
partition.
If
you
can't
receive
message
from
the
threshold
quorum
of
participants
in
the
VAT,
you
cannot
see
progress
now.
A
When
you
get
into
massive
multi
way
replication,
then
you
have
a
lot
of
the
high
availability
properties
that
were
used
to
for
block
chains.
So
at
this
level,
with
regard
to
the
individual,
that's
nothing
were
saying
changes
the
availability
characteristics
under
partition.
It's
just
sort
of
standard
quorum
issues
with
regard
to
partition,
with
our
fabric
going
between
them.
The
fact
that
the
messages
are
individually
signed
and
can
be
delivered
later
means
that
if
there
is
a
partition,
traffic
can
just
accumulate
to
be
delivered
later
when
the
partition
heals.
A
A
So
all
three
layers
is
like
a
triple
decker
bus
of
messages,
so
I'll
treat
all
three
layers
see
exactly
the
same
incoming
order
of
messages
and
that's
good,
because
the
three
green
wires
they're
doing
the
same
kind
of
job,
but
they
don't
need
to
do
it
in
sync.
The
three
blue
layers
have
to
be
exactly
perfectly
in
sync,
because
that's
where
the
validation
comes
in,
that
they're
reproducing
exactly
the
same
computation
yeah.
B
A
One
is
for
somebody
outside
the
VAT
deciding
whether
the
VATS
didn't
said
something
what
threshold
they
should
use
and
then
there's
within
the
consensus
mechanism
of
that
what
consensus
will
should
be
used
and
those
can
use
different
thresholds.
Those
don't
need
to
be
coupled,
but
often
you
know,
you'll
be
making
the
same
decision
across
both.
A
A
A
But
then
it
also
included
the
give
to
as
an
opaque
payload
that
got
carried
so
that
when
the
take
from
went
to
that
see,
it
also
carried
to
give
to
just
in
case
so
that
it
could
be
so
that's
to
ensure
that
it
gets
delivered
earlier.
But
the.
But
the
key
thing
is
that,
logically,
every
message
says:
what
is
the
tale
of
the
causality
chain
of
messages
that
must
be
delivered
ahead
of
that
one.
A
So
every
message
has
a
cumulative
hash
of
the
tree
of
early
met
earlier
messages,
and
that
way
you
ensure
that
a
message
does
not
get
honored
unless
all
of
the
earlier
messages
needed
to
show
that
it
that
that
the
cumulative
hash
is
correct.
Until
you
see
that
cumulative
hash
validate
you
don't
honor
the
message.
A
A
At
every
level
of
abstraction
here
there
are
adapters
and
the
adapters
each
have
their
own
tables.
The
red
adapters
might
be
routing
tapers
and
tables
network
fabric
or
a
distributed
hash
table
or
whatever
we're
not
that
we're
gonna.
That's
the
last
we're
gonna
mention
the
routing
fabric,
we're
going
to
focus
in
on
the
green
adapters,
which
are
cryptographically
how
one
that
talks
to
another.
A
A
So
let's
say
that
the
messages
from
A
to
B
excuse
me
a
to
b,
arrive
first
and
now,
they've
arrived
at
the
the
forum
mechanism
has
candidate
messages
to
be
delivered.
Next,
let's
say
that
that
they're
accepted
the
top
host
there
be
computation
calculates
that
outgoing
message
that
gets
similarly
hits
the
fan
out
device.
But
now
this
is
the
first
time
that
that
B
has
heard
of
that
C.
So
this
is
when
it
builds
those
tables.
It
then
contacts
that
C,
which
is
the
first
time
that
C
has
heard
of
that
D.
A
And
then
the
message
gets
multicast
to
both
of
the
hosts
of
that
see
into
the
incoming
three
to
one
fan
in
device,
which
is
the
thing
that
gathers
evidence
towards
hypothesis
that
the
VAT
as
a
whole
said
something
seeing
that
one
of
the
the
hosts
contributing
to
that
be
claimed
that
it
said
something
is
evidence
that
that
be
said
something,
but
it's
not
definitive
evidence,
not
conclusive.
So
that
message
is
stuck
there
waiting
for
more
evidence.
However,
the
ADA
see
message
being
emitted
from
that
a
needs,
no
further
evidence
so
being
carried
along.
A
Carries
through
the
rest
of
it
that
gets
delivered
to
the
quorum
mechanism
and
process.
So
now
that
that
message
has
been
safely
processed,
we
still
have
to
stock
messages,
and
that's
because
only
one
of
the
three
the
hosts
has
actually
process
has
actually
done
the
computation.
So
let's
say
that
b2
proceeds
sends
the
same
message
into
the
fan-out
device
that
hits
layer
and
now.
A
A
A
The
intern,
not
the
internal
structure,
you
need
to
know,
as
matter
of
fact,
that's
the
perfect
segue
for
this
slide.
It's
like
the
perfect
question,
so
so
it's
the
definition
of
the
VAT
is
explaining
how
to
talk
to
it,
and
so,
when
you
learn
the
name
of
the
VAT,
you
know
what
devices
to
build
in
order
to
talk
to
the
bat.
So
this
is
a
special
case
of
a
very
general
technique
that
sometimes
referred
to
as
self-authenticating
designators
things,
whose
name
explains
to
someone
holding
the
name.
A
What
decision
procedure
to
use
to
determine
if
a
particular
thing
is
the
thing
that
the
name
designates
so
the
most
familiar
example
of
this
is
a
cryptographic
hash.
So
when
you
just
have
a
snapshot
of
data,
if
you
name
the
data
with
the
hash
of
the
data
which
all
of
the
system
shown
the
parens
there
do,
then
anyone
knowing
that
name
knows
what
to
do
when
presented
with
data.
A
A
So
with
the
VAT
ID,
the
VAT
is
not
data.
It's
an
active
computational
entity,
so
the
problem
we
have
to
solve
is
somewhat
different.
There's
two
sub
problems,
the
name
my
name
has
to
explain
how
to
talk
to
me,
and
my
name
has
to
explain
how
to
listen
to
me.
So
on
the
talking
it's
you
know
cryptographically.
A
So
in
the
history
of
this
model
of
computation,
which
goes
back,
a
very
long
ways
goes
back
to
the
mid
90s.
Actually,
all
of
those
previous
systems
were
using
live,
TLS
connections
and
a
live
TLS
connection
because
of
its
symmetry
because
of
its
by
directionality.
It
solves
the
whole
problem
for
both
sides
in
one
mechanism,
but
because,
exactly
because
of
its
one
for
one
live
connection
nature,
it
doesn't
generalize
into
the
world
we're
trying
to
fill
so.
Instead,
we
sign
individual
messages.
A
A
As
we've
seen
a
quorum
that
can
get
the
name
of
the
Corvette
can
list
the
public
keys
of
the
participants,
the
hosts
that
are
contributing
and
can
state
the
threshold
rule.
Any
two
out
of
three
of
these
enumerated
participants
are
what
it
means
for
this
VAT
to
have
done
something:
that's
the
meaning.
That's
the
the
name
of
the
VAT
is
the
authenticity
award
and
then,
of
course,
that's
a
step
towards
blockchains.
A
The
device
you
have
to
construct
for
talking
to
a
blockchain
is
essentially
a
light
client
for
whatever
the
light
client
is
for
sending
messages
into
that
blockchain
and
that's
very
nice,
because
it's
light,
unfortunately,
to
really
listen
to
a
blockchain
securely
and
determine
what
it's
said
in
a
definitive
manner.
The
listening
device
has
to
be
more
like
a
full
node
and
for
block
chains
like
etherium
that
don't
have
finality
you
have
to
in
to
a
particular
build
in
front
of
it
of
finality
threshold.
Again,
a
linear
s.
Holding
today.
B
A
So
that's
the
the
end
of
part.
One
we've
gone
through
these
three
layers.
Next,
we're
going
to
talk
about
the
actual
smart
contracting
layer.
Now
that
we
have
the
Foundation's,
we
understand
why
distributed
secure
objects
can
work
across
the
whole
system.
So
if
anybody
has
further
questions,
they'd
like
to
ask
here.
B
A
So
one
of
the
interesting
things
about
a
VAT
which
I
didn't
mention
is
that
the
VAT
is
also
the
unit
of
portability
or
the
unit
of
migration,
and
when
you
migrate
a
VAT,
the
blue
level
is
the
thing
that
you
have
to
snapshot
and
migrate.
The
green
level.
You
have
to
rebuild
a
new
one
around
the
blue
level,
because
that's
very
dependent
on
weird
that
that
is
both
both
yeah.
What
it's,
what
it's
being
hosted
on,
as
well
as
from
there?
A
How
it
talks
to
the
other
things
that
talks
to,
but
the
fact
that
the
blue
layer
can
be
snapshotted,
moved
and
reconstituted
is
really
very,
very
cool
and
because
of
the
storm
forward
nature
of
the
messages
once
it's
revived
the
old
messages
that
are
outs
that
are
outstanding
to
it.
If,
assuming
that
they
get
routed
correctly,
the
underlying
object
message
within
those
messages
does
get,
does
get
delivered
and
computation
just
continues
transparently
after
the
migration.
B
B
A
A
The
we
are
I'm,
sorry,
the
question
is:
do
we
have
tools
that
we
use
to
verify
security
properties
of
smart
contracts?
So
the
answer?
The
answer
yes
was
premature.
This
is
a
a
long
term
activity,
but
we
have
been
collaborating
with
some
academic,
formal
methods.
Researchers.
Now,
for
several
years,
the
quote,
the
closest
collaboration
is
with
largest
name-drop
Sofia
Drosophila
Imperial
College
James
Nobel
of
New
Zealand
and
Toby
Marie
of
the
SEL
for
data
61.
A
So
so,
even
though
we've
been
working
on
that
for
years,
it's
going
to
be
a
while
before
that
that
that
gives
us
any
kind
of
tooling
for
form
of
verification.
However,
the
really
important
thing
for
the
present
is
that
the
activity
of
working
on
that
on
the
side
ensures
that
the
semantics
of
the
rest
of
our
system
stay
clear
and
simple.
It
ensures
that
we
don't
confuse
ourselves
because
the
formal
methods
work.
A
So
we've
already
seen
Oh
caps
object
references
being
permissions
well
permission
permission
to
invoke
an
object
is
a
kind
of
right.
So
so,
when
we
talk
about
building
a
rights
on
top
of
Oh
caps,
what
are
the
what's
the
difference
in
the
kind
of
right
that
we
would
build
as
opposed
to
the
kind
of
right?
We
already
have
we're
going
to
be
building
the
new
ones
as
a
pattern
on
top
of
the
old
ones,
but
the
new
ones
have
their
own
character
so
on
the
Left.
A
There's
exercise
versus
symbolic
objects
are
all
about
the
exercise
right.
You
exercise
a
right
when
you
actually
do
something
with
the
right
I'll
like
invoke
the
object
provoking
its
behavior,
whereas
money
is
just
symbolic,
it
doesn't
do
anything.
It's
only
valuable
because
of
the
expectation
that
you
can
create
it
to
others
who
will
in
turn
value
it.
A
An
object
by
default
is
opaque
when
Bob
receives
the
Carol
argument.
He's
just
received
some
object
from
someone
who
could
send
the
messages
he
doesn't
know
what
the
object
is.
He
can
provoke
its
behavior,
but
he
doesn't
know
what
behavior
doesn't
necessarily
know
what
behavior
to
expect.
It
requires
more
patterns
for
Bob
to
be
able
to
form
such
expectation,
whereas
on
the
right
again,
Bob
doesn't
consider
himself
to
be
paid
unless
he
knows
what
it
is.
That
he's
got
what
it
is
that
he's
received
the
exclusive
right
and
then
there
is
specific
versus
fungible.
A
A
Now,
it's
not
that
he
writes
represent
just
the
right-hand
side
that
just
the
right-hand
column,
o
caps
represent
just
the
left-hand
column
that
part's
true.
But
this
contrast
is
showing
us
a
taxonomy
with
multiple
dimensions,
and
we
want
a
language
for
talking
about
electronic
writes
that
covers
all
the
dimensions
of
variation
described
by
this
taxonomy.
A
So
this
is
the
age
old
Mint
maker
example.
That's
been
repeated
in
the
object
capability
community
now
for
at
least
20
years,
and
the
beautiful
thing
about
this
example
with
regard
to
the
taxonomy
you
just
saw
is
that
this
is
all
of
the
code
needed
to
build,
writes
that
have
all
of
the
attributes
we
saw
on
the
right-hand
column
out
of
object
capabilities
that
have
the
attributes
in
the
left-hand
column.
A
A
She
wants,
to,
let's
say,
buy
tickets
from
him
and
when
Bob
gets
the
buy
message
at
this
point
he
all
he
knows
is
he
received
an
alleged
payment,
but
he
asked
he
sends
to
his
main
purse,
this
deposit
method
and
when
the
posit
method
acknowledges
that
the
deposit
was
good.
Bob
now
knows
he's
been
paid
without
trusting
Alice
and
can
release
the
concert
ticket.
This
fully
protects
Bob
from
Alice,
but
it
does
not
protect
Alice
from
Bob
Bob
could
just
pocket
Alex
Alice's
money
and
then
not
give
a
concert
ticket
in
exchange.
A
Smart
contracts
are
generally
about
the
exchange
of
rights,
and
we
need
to
know
that
both
parties
have
received
the
rights
that
they
were
looking
for,
that
they
were
expecting
in
exchange
for
the
rights
they
were
offering,
and
otherwise
that
nothing
happens
either.
Both
parties
are
satisfied
or
everything
is
unwound
and
it's
as
if
the
exchange
was
never
cried.
In
the
first
place.
A
A
So
that's
the
deposit
method
we
see
over.
There
is
a
particular
in
order
to
bring
about
the
exclusive
transfer.
What
we
need
to
do
is
reconstruct
that
purse
example
as
writes
implementing
this
abstract
interface
and
the
key
thing
about
this
abstract
interface.
Is
that
writes
across
the
entire
taxonomy,
including
especially
the
attributes
of
exclusivity
and
the
attributes
of
a
say,
being
able
to
know
what
it
is.
You
got
that
rights
across
that
taxonomy
can
all
be
implemented
in
such
a
way
that
they're
described
by
the
e
RTP
protocol
and
the
e
RTP
protocol.
A
This
set
of
object
interfaces
now
enables
us
to
build
oh
I'm,
sorry
and
this
over
here.
This
is
actually
the
reconstruction
of
the
Perce
implementation.
It's
a
little
bit
more
code,
not
a
frightening
amount
of
more
code
in
order
to
take
the
same
logic
and
embed
it
in
this
very
general
description
of
the
RTP
and
the
result
of
doing
that
is.
We
can
now
create
generically
parameter
risible
contracts,
contracts
like
an
escrow
exchange
contract
that
handle
any
write
that
is
presented
through
the
e
RTP
protocol.
A
A
This
is
very
much
like
an
escrow
exchange,
except
that
Bob's
tickets
are
pre,
escrowed
and
Bob
has
lost
the
ability
to
cancel
before
the
deadline
and
the
escrow
exchange.
Alice
and
Bob
could
cancel
at
any
time.
The
current
call
is
built
out
of
the
escrow
exchange,
primarily
by
the
pre
escrowing
of
the
tickets,
and
by
taking
the
cancel
ability
and
putting
it
in
the
game,
clock
lat,
rather
than
giving
it
to
Bob
so
until
the
deadline
Bob
cannot
cancel.
Now.
A
The
ability
to
play
the
contract,
while
that
is
in
motion
to
play
the
contract
prior
to
the
deadline,
is
itself
valuable
for
the
next
week.
Alice
could
spend
the
money
to
buy
Bob's
concert
hands,
but
let's
say
that
Alice
finds
out
that
she
has
a
conflict.
Then
she
can't
actually
go
to
the
concert
anyway.
Well,.
A
So
if
Alice
wants
to
sue
to
sell
the
option
to
get
the
contract,
the
concert
tickets
to
Fred,
she
can
just
use
the
the
contracting
framework
around
the
covered
call
as
an
issuer
of
the
right
to
to
participate
in
the
contract
as
the
Alice
side
of
the
contract
and
and
then
that
becomes
an
issuer
of
the
RTP
described
rights
into
any
further
contract
that
can
operate
on
any
er.
Tp
described
right.
A
So
this
is
fundamentally
powerful
in
a
way
that
should
be
familiar
to
us
from
our
object-oriented
and
functional
programming
paradigms,
which
is
object.
We
build
abstractions
for
manipulating
objects
and
then
we
package
those
abstractions
as
objects
which
can
thereby
be
manipulated
by
other
objects,
and
when
we
create
a
generic,
we
parameterize
Abul
abstraction
like
a
table
that
you
can
put
any
object
into
and
take
it
back
out
of
then
that
becomes
higher-order.
A
It
is
itself
the
kind
of
thing
that
it
can
manipulate.
It
can
manipulate
objects,
irrespective
of
what
other
objects
those
are
manipulating.
So
there's
there's
and
and
it's
that
higher-order
nature
of
functions
and
objects
that
leads
to
the
composability
that
has
created
the
richness
of
the
modern
software
industry
and
large
rich
frameworks
and
object-oriented
libraries
and
compositions
of
them.
The
compositionality
of
software
is
built
out
of
that
higher-order
nature.
B
B
A
A
The
important
thing
about
the
full
methods
work
that
we've
been
doing
is
we've
been
able
to
analyze
these
contracts
and
show
that
they're
correct
that
they
do
the
job
that
we
specified
and
that
they
compose
with
other
contracts
that
we
don't
need
to
describe
beyond
the
assumption
that
they
are
constrained
by
object,
capability
rules
and
and
the
constraint
by
object.
Ability
rules
means
that
you
don't
have
to
reason
about
their
code.
You'd
have
to
reason
about
their
behavior.
A
You
have
to
reason
about
the
fact
that
limit
on
their
behavior
is
the
capabilities
that
they've
been
granted
because
the
capabilities,
the
object
references
are
the
only
means
by
which
an
object
gets
to
cause
effects
on
the
world
outside
of
itself.
And
that's
why
we're
able
to
do
such
deep
composition
with
confidence.
B
B
B
A
A
There's
just
a
lot
of
language
design
on
coming
up
with
good
specification
languages,
and
it's
not
just
the
formal
issues
on
good
specification
language,
one
of
the
things
that
we've
been
very
disappointed
with,
where
I
personally
would
say.
I'll
just
speak
for
myself
very
disappointed
with
with
regard
to
a
lot
of
other
formal
methods.
Work
is
the
specifications
themselves
are
very
complicated,
they're
more
complicated
than
programs.
A
That
I
already
have
a
hard
time
understanding,
and
if
I
can't
understand
the
specification,
then
we've
just
moved
the
problem
from
what
is
my
programming
into
the
problem
of
what
modes?
What
does
my
specification
so
one
of
the
arts
of
writing
a
specification
language
is
that,
just
as
we
want
to
program
in
a
way
that
supports
both
informal
and
normal
reason,
we
want
to
formally
specify
in
a
way
that
supports
both
informal
and
formal
spent
reasoning
about
the
meaning
of
the
specification
and
that's
where
a
lot
of
the
iteration
comes
from.
A
But
with
regard
to
the
particular
example,
you
raised
yes,
what
we've?
What
what
our
specification
is
able
to
specify
and
what
we've
been
able
to
prove
the
per
system
or
Bayes
is
without
a
purse?
You
cannot
affect
its
balance
with
two
purses.
You
can
move
money
between
them,
but
you
cannot.
You
cannot
effect
conservation
of
currency
with
a
mint.
A
A
That
a
deposit
reporting
success
means
that
the
invoker
of
the
deposit
Bob,
depositing
Alice's
money
that
Bob
can
trust
that
he
has
actually
received
an
exclusive
on
the
described
amount
of
money.
You
can
trust
that,
to
the
same
extent,
that
he
trusts
the
purse
he
deposited
it
into
so
there's
this
and
that
sort
of
the
that
turned
into
turned
out
to
be
the
crucial
lever
for
the
family
thing
is
propagation
of
contingent
crust
and
suspicion
relationships.
We
don't
know
if
Bob
trusts
his
main
purse,
but
to
the
degree
that
he
trusts
his
main
purse.
A
A
A
Given
these
preconditions-
and
this
thing
happens,
these
are
the
post
conditions,
but
normal
logic
is
good
for
reasoning
about
sufficient
conditions
that
if
these
things,
you
know
that,
if
you
have
the
following
set
of
conditions,
then
you
expect
the
following
result:
they're
very
bad
at
reasoning
about
necessary
conditions,
because
in
order
to
say
well,
if
this
thing
happened,
let's
say
if
the
total
amount
of
currency
was
increased,
then
somebody
must
have
called
the
mint
okay.
You
can
only
reason
about
that,
in
normal
logic,
by
doing
an
induction
over
all
of
the
things
you've
specified.
A
So
what
we've
done
is
we've
extended
to
logic,
to
be
able
to
speak
compliant,
compactly
about
necessary
conditions
as
well
as
sufficient
conditions
and
we've
also
added
one
more
clause.
Besides
preconditions
and
postconditions
there's
a
another
clause
which
are
the
conditions
that
must
be
true
at
every
step
between
entry
and
exit,
those
conditions
that
cannot
be
violated
even
momentarily
in
getting
from
the
entry
to
the
exit
that
turned
out
to
the
that's.
Not
tremendously
interesting,
but
it
turned
out
to
really
ease
a
lot
of
our
verification.
A
I'm
sorry
they're
repeating
the
question.
Thank
you.
Thank
you
for
audience
signals
to
repeat
the
question.
Please
keep
doing
that.
Do
I,
expect
that
we'll
be
able
to
do
this
purely
with
static
analysis
or
do
I
expect
that
there
will
be
a
role
for
its
extra
runtime
enforcement,
and
the
answer
is
mixed.
A
A
However,
the
in
order
to
have
a
program
that
is
easier
to
statically
reason
about
with
an
out-of-band
specification.
If
the
program
itself
does
some
enforcement,
that
enforcement
can
in
turn
ease
the
burden
on
the
specification
and
then
the
tooling
eventually
can
go
from
the
failure
to
verify
to
suggested
enforcement
mechanisms
to
to
aid
the
verification
effort.
But
this
is
this
is
way
ahead
of
where
we
are
right
now.
B
A
In
order
to
transfer
money
between
the
purses,
there
has
to
be
a
moment
where
currency
is
not
conserved,
that
you
have
to
change.
One
balance
before
you
change
the
other
balance.
So
how
do
you?
How
do
we
write
that
and
ensure
that
we
that
the
way
in
which
it's
written
cannot
cause
an
observable
violation
of
conservation
of
heart
sitting,
so
actually
I'm
gonna
go
to
work?
Are
we
current
there's
no
reason
for
me
to
use
the
old
code.
A
The
critical
element
that
I
have
not
that
I've
alluded
to,
but
I
haven't
really
stressed,
is
that
our
overall
computational
model
is
communicating
event
loops
where
each
turn
of
the
event
loop
is
a
separate
transaction
and
the
computation
that
happens
during
the
transaction
is
simple,
sequential
imperative,
computation.
So
there's
no
fine-grained
shared
memory,
multi.
A
A
The
purses
are
registered
in
the
ledger
on
the
lower
right
with
the
ledger
got
set,
so
only
purses
of
this
issuer
of
this
currency
get
to
be
in
this
ledger.
Every
time
you
make
a
new
mint,
you
make
a
whole
new
system
of
currency
with
its
own
ledger,
so
the
ledger
dot
get
of
purse.
Well,
that's
that's
this
person
set,
which
is
the
find
that
their
cost
purse
equals
death,
open,
paren,
open,
curly
and
inside
make
her
see.
That's
the
purse,
that's
references!
That's
my
own
balance
net
is
a
is
a
utility
function.
A
It
just
checks
that
the
argument
has
the
value
of
a
natural
number
within
the
range
of
safely
representable
natural
numbers.
Javascript
will
have
big
int
soon,
in
which
case
this
first
line,
the
Outernet
and
his
first
line
will
become
unnecessary,
but
right
now
the
safe
range
of
natural
numbers
as
a
is
the
range
of
floating-point
numbers.
So
this
first
line
the
net
on
the
right
is
necessary.
It's
saying
ensure
that
what
I've
been
handed
as
our
argument
is
a
natural
number.
A
The
outer
nap
on
the
first
line
is
saying
make
sure
the
result
of
adding
these
things
together
does
not
overflow.
That
goes
away
once
you
have
begins
on
the
second
line.
We
look
up
this
the
alleged
first
verse.
The
second
argument
in
the
ledger:
if
the
serous
purse
isn't
is
anything
other
than
a
purse
of
this
currency
that
lookup
fails
and
if
that
lookup
fails,
then
the
math
around
that
fails.
A
It
fails
with
an
exception
and
you
abort
at
that
point,
and
if
the
lookup
succeeds-
and
you
have
a
balance,
then
you
subtract
amount
from
that.
You
already
know
amount
as
a
natural
number.
If
the
result
is
not
a
natural
number,
then
you're
overdrawn-
and
you
get
another
exception
at
that
point.
You've
done
all
of
the
checks
that
might
fail
and
because
the
remaining
part
of
the
transaction
has
nothing
that
can
fail,
it
can
now
do
a
set
of
side
effects
and
because
no
failure
can
happen
between
them.
A
The
side
effects
that
remain
into
transaction
are
effectively
atomic.
They
happen
before
anything
else
can
observe.
So
it
sets
the
source
purses
balance
to
the
decremented
balance.
It
sets
this
person
balanced
at
the
incremented
balance
and
I
will
leave
as
a
as
a
puzzle
through
the
audience.
Why
my
recompute
on
that
last
line
the
incremented
balance,
rather
than
remembering
it
from
the
first
line,
but
that's
the
atomicity
issue,
and
but
but
the
result
is
that
yes
moment,
Harold
Lee
done.