►
From YouTube: Towards Formally Verified Smart Contracts with Haskell - Allison Irvin & Nick Waywood, IBM
Description
Towards Formally Verified Smart Contracts with Haskell - Allison Irvin & Nick Waywood, IBM
In enterprise DLTs, smart contracts implement security critical and business critical logic. Therefore there is a clear need to have confidence that smart contracts adhere to the intended specification, without any errors, bugs or malicious code. Events like the DAO attack on the Ethereum blockchain in 2016 is unacceptable in a permissioned, enterprise solution. In order to guarantee the correctness of a smart contract, formal verification is necessary. Because of this, there is a strong research focus in the wider blockchain community on enabling formal verification of smart contracts written in functional programming languages (e.g. DAML, Liquidity, F*, Elle, Verisol, etc.). Functional programming languages lend themselves well to formal verification due to the fact that both formal verification and functional programming have their roots in mathematics. However, to date, little work within the Hyperledger community has been done on bringing formal verification to smart contracts on Hyperledger DLTs.
This talk presents support for writing Hyperledger Fabric chaincode with Haskell, a big first step towards having fully verified and secure smart contracts. The work is evaluated by comparing contracts written in Go, Java and Node with Haskell to demonstrate how a functional programming language can help identify flaws in logic, leading to code that is both correct, secure and easier to reason with. The talk finally demonstrates how smart contracts written in Haskell can be formally verified.
----
Hyperledger – Open Source Blockchain Technologies
Hyperledger is an open source community focused on developing a suite of stable frameworks, tools and libraries for enterprise-grade blockchain deployments.
It serves as a neutral home for various distributed ledger frameworks including Hyperledger Besu, Fabric, Sawtooth, Indy, as well as tools like Hyperledger Avalon, Cactus and libraries like Hyperledger Aries, Ursa. Learn more about Hyperledger projects: https://www.hyperledger.org/use
Case Studies: https://www.hyperledger.org/learn/case-studies
Training & Certification: https://www.hyperledger.org/learn/training
Tutorials: https://www.hyperledger.org/use/tutorials
Webinars: https://www.hyperledger.org/learn/webinars
Events: https://www.hyperledger.org/events
Vendor Directory: https://www.hyperledger.org/use/vendor-directory
Subscribe to the Hyperledger Newsletter: https://www.hyperledger.org/newsletter
Follow-us on Twitter @Hyperledger
Learn about Hyperledger Membership: https://www.hyperledger.org/about/join
#Hyperledger #HyperledgerGlobalForum2020 #Blockchain
A
A
So
the
talk
we're
giving
today
is
split
up
into
two
main
sections:
I'm
gonna
be
presenting
the
first
section
where
I'm
going
to
be
talking
about
the
importance
of
correctness
and
smart
contracts.
That's
essentially
explaining
the
plot,
the
purpose
of
formal
verification
in
the
context
of
why
we're
doing
the
work
that
we've
done
so
far
and
the
second
section
Alison
will
be
presenting
which,
where
she
will
be
taking
you
through
the
work
that
we've
been
working
on,
what
we've
done
so
far
for
building
a
foundation
for
this
formal
verification
in
hyper
ledger
fabric.
A
So
to
explain
the
importance
of
correctness
and
smart
contracts.
I
want
to
give
some
context
by
explaining
DL
T's
in
the
condom
at
D.
Lt
is
as
critical
systems.
So
in
the
world
of
software,
some
systems
are
classified
as
critical
systems
and
some
examples
of
this
safety
critical
systems.
So
the
classic
example
of
a
safety
critical
system
is
aeroplane
software,
but
it's
any
software
where
there's
a
threat
to
human
life.
A
Classic
example,
there
is
stock
exchanges
and
there's
also
security,
critical
software
security,
critical
systems
or
any
systems
where
they
have
sensitive
information
and,
and
they
include
banking
systems
and
government
systems
and
obviously
a
lot
of
systems
like
that
and
critical
systems.
The
code
needs
to
be
treated
in
a
much
more
rigorous
way
than
in
non-critical
code
to
ensure
that
it
does
what
it's
intended
to
do.
A
So,
in
specifically
in
terms
of
blockchain
I
want
to
talk
about
trust,
so
got
a
simple
picture
here
of
a
blockchain
and
the
thing
one
of
the
main
selling
points
of
the
blockchain
is
that
it's
a
trusted
single
source
of
truth,
and
this
trust
comes
from
the
fact
that
there's
a
ledger
of
all
the
transactions
that
have
happened,
and
this
is
immutable.
But
how
that
works,
though,
is
we
have
a
small
contract
here
that
the
transactions
come
through
and
it's
the
smart
contracts
that
actually
write
all
the
information
onto
the
ledger?
A
Because
of
that,
when
we
talk
about
trusting
a
ledger
that
doesn't
really
make
any
sense,
if
you
don't
actually
trust
a
smart
contract
and
therefore
the
code,
that's
in
that
smart
contract.
That
is,
writing
the
information
into
the
ledger.
So,
to
tie
this
back
to
what
I
was
saying
about
critical
systems
since
block
chains
or
critical
systems,
you
need
to
be
able
to
trust
the
smart
contracts,
since
they
are
the
ones
that
are
kind
of
governing
the
trust
in
the
network.
A
A
So
in
talking
about
this
trust,
what's
the
problem
with
the
current
smart
contract
languages
to
achieve
this?
So
for
those
who
aren't
overly
familiar
with
fabric,
we
currently
support
three
smart
contract
languages,
golang
java
and
javascript,
and
these
are
all
general-purpose
imperative
languages
and
these
languages
are
prone
to
exploits
in
bugs
that
are
not
well
suited
for
critical
systems.
A
If
you
can't
trust
the
smart
contracts,
because
I
mean
her
like
financial
markets,
like
they
work
with
a
demo,
but
also
other
industries
that
are
critical
systems,
you
need
to
be
able
to
trust
the
blockchain
and
the
smart
contracts
and
not
introduce
new
sources
of
risk
into
your
domain.
So
talking
about
this,
how
can
these
problems
be
solved?
A
A
Yep,
so
let's
see
I'm
saying
function.
Programming
is
the
solution
right
now,
but
I
haven't
explained
how
at
all.
So,
let's
go
into
that.
So
we're
saying
to
trust
the
ledger
into
trust
the
blockchain.
You
want
to
need
to
be
able
to
trust
your
smart
contracts
and
your
smart
contracts
are
essentially
just
code.
So
how
can
you
trust
your
code
so
at
the
bottom
here
you
can
see.
A
A
A
We
agree
with
Dijkstra,
so
EDX
good
Dijkstra
here
is
a
famous
computer
scientist
from
the
1960s
who's
done
a
lot
of
work
around
distributed
systems
as
well
as
formal
verification,
and
this
quote
is
essentially
saying
when
you're
writing
tests,
you're
testing,
specific
instances
of
a
runtime
of
a
function
or
some
piece
of
software,
and
you
can
sequentially
eliminate
some
certain
executions
of
that
function
to
be
incorrect.
But
you
can
never
prove
ibly
know
that
there
are
no
bugs
in
the
system.
A
So
that
being
said,
don't
get
me
wrong.
We're
not
saying
testing
is
bad
and
it
shouldn't
be
in
the
software
engineering
industry.
That's
not
true
at
all.
It
definitely
has
its
place,
but
we
don't
believe
that
places
in
critical
systems
where
the
correctness
is
more
important
than
some
everyday
software.
A
B
A
What
is
form
of
verification?
Talking?
I've
been
mentioning
it
a
few
times,
so
I've
got
the
definition
at
the
top.
I
won't
read
that,
but
essentially
what
it
does
is
you
have
a
formal
specification
which
specifies
how
a
certain
piece
of
code
should
behave
and
how
it
is
correct,
and
that
specification
will
then
under
the
hood,
use
what
are
called
formal
methods
to
then
mathematically
prove
that
the
code
you
were
writing
a
specification
for
is
doing
what
it's
intended
to
do.
A
So
this
is
the
inverse
of
testing
where,
rather
than
just
like,
I
mentioned
one
of
the
time,
eliminating
certain
input
values
that
could
be
incorrect
with
the
code,
you're
mathematically,
exploring
the
whole
state
space
of
a
function.
Mathematically
and
the
other
important
thing
about
this.
This
will
happen
statically
and
not
at
runtime
and
you'll
get
a
guarantee
whether
the
code
is
conforming
to
that
specification
or
not.
A
So
one
of
the
main
popular
techniques
for
performing
travel,
formal
verification
is
called
designed
by
contract
and
essentially
the
contract
is
the
specification
that
I
was
mentioning
on
the
previous
slide
and
that
contract
will
have
certain
things
in
it.
These
top
points
down
below
that
would
specify
how
a
function
needs
to
behave
so
preconditions
essentially
just
guarantees
on
a
certain
properties
for
the
input,
values
of
a
function
and
similarly
post
conditions
for
the
output,
values
and
then
invariance.
A
So
you
can
specify
some
property
in
our
case,
whereas,
wherever
have
to
see
an
example,
will
be
a
function
and
throughout
the
lifetime
of
that
function
we
can
specify
some
property
that
will
be
constant
throughout
the
whole
lifetime
of
that
function
and
that's
useful
for
preventing
bugs
and
exploits,
and
we're
going
to
look
at
an
example
of
an
invariant
right
now
and
invariant
that
could
have
prevented
the
DAO
attack.
So
here
I
have
a
simple
solidity
contract.
A
A
So
this
is
the
intended
execution
of
this
contract
and
how
the
developer
of
this
contract
intended
it
to
work.
So
on
that
line
five,
where
they
do
that
call
and
withdraw
the
amount
that
goes
to
an
end-user
who
receives
that
money
and
then
after
they
receive
the
money,
the
function
call
will
return
back,
and
then
this
shares
will
get
updated
after
that.
A
It
can
actually,
while
the
runtime
of
that
contract,
is
being
executed,
the
fund
contract,
they
can
actually
re-enter
and
call
back
into
the
function
and
keep
doing
that
and
drain
the
money
of
the
out
of
the
account
and
this
process
of
a
malicious
contract
receiving
a
call
like
on
line
five
and
re-entering
into
the
contract.
Well,
it's
still
executing
is
essentially
how
the
DAO
attack
happened.
So
how
could
we
have
prevented
such
a
thing
happening?
This
is
the
same.
Exactly
the
same
contract,
but
instead
I've
specified
an
invariant
on
line
one.
A
This
is
a
pseudo
code,
so
this
is
not
absolutely
how
you
would
write
it,
but
just
for
simplification
and
to
show
the
concept.
I
turned
it
into
pseudo
code,
but
basically
this
invariant
is
saying
that
the
amount
of
shares
in
the
fund
minus
the
current
uses,
user
balance
needs
to
stay
constant
throughout
the
runtime
of
this
function
and
because
of
that
and
like
I
mentioned
before
this
formal
verification
happens
statically
at
one
time
with
that
invariant
in
place.
A
So
this
invariant
kind
of
saves
you
and
what
it
will
tell
you
is,
if
you
just
put
the
shares
so
here
down
on
line
eight,
we
have
shares
minus
equals
amount.
If
we
put
that
before
the
call,
so
the
team
that
shares
data
gets
updated
before
the
call,
then,
if
that
reentry
happened,
it
would
fail,
because
the
invariant
sorry
I
explained
that
not
quite
right,
because
the
shares
amount
is
before
now.
The
raintree
check
can
occur
because
if
the
call
came
back
in
it
wouldn't
work
because
the
shares
had
already
been
updated,.
A
A
The
current
state
of
the
art
for
ensuring
correct
code
is
functional,
programming
and
formal
verification
and
the
ability
to
have
confidence
in
smart
contracts
conference
that
they
are
correct.
We
believe,
is
worth
creating
a
new
contract
language
for
so
before
I
hand
it
over
to
Allison
to
show
you
through
the
work
we've
done
so
far.
First,
the
tie
it
all
up
I
want
to
give
a
brief
introduction
to
functional
programming
in
Haskell.
A
So,
for
those
that
aren't
familiar,
the
the
core
concept
behind
functional
programming
is
that
your
whole
programs
that
build
up
of
mathematical
functions
and
mathematical
function
has
a
few
different
names.
You
may
have
heard
it
called
a
pure
function
or
a
deterministic
function,
and
they
all
mean
the
same
thing.
A
A
I'm
so
jealous
tration
of
that
just
at
the
bottom
here,
so
a
pure
function
give
it
an
input,
and
the
output
will
always
be
the
same.
However,
with
an
impure
function,
other
things
can
happen
as
well,
when
these
other
things
that
could
happen
that
could
change
the
result.
Each
time
are
called
side
effects.
A
The
fact
that
they
have
to
be
pure
functions
means
that
running
side-effects
in
the
program
have
to
be
controlled
by
controlled
and
managed
by
the
language
runtime,
which
is
an
important
point
for
formal
verification
as
well,
which
we'll
get
to
later,
as
well
so
side
effects.
So
the
reason
we
call
them
side
effects
is
because
in
mathematical
function,
terminology
there's
a
main
effect
and
the
main
effect
of
a
function
is
returning
a
value.
A
The
output
value
of
the
function,
so
anything
else
that
the
function
does
that
is
observable
outside
the
scope
of
the
function
is
Cliff's
classified
as
a
side
effect,
so
examples
of
that
performing
I/o,
mutating
data,
or
even
just
calling
another
function
within
itself.
That
in
turn
performs
some
side
effects.
A
A
So
this
function
is
just
an
add
name
function
that
will
add
a
new
name
to
an
array,
the
array
up
on
line
1
and
you
can
see
on
line
4.
So
that's
already
a
side-effect.
It's
accessing
a
global
variable
outside
of
its
own
scope,
and
then
it's
performing
another
side
effect
on
line
5.
So
it's
doing
some
IO
operation.
A
We
have
no
idea
what
it's
doing,
but
it's
doing
something
and
then
returning
a
boolean,
and
that
therefore
was
a
side
effect
and
then
on
line
7
we're
mutating
the
global
variable
based
off
that
boolean,
that's
returned
from
that
IO
operation
and
furthermore,
this
function
doesn't
even
have
a
main
effect.
There's
no
return
value,
so
the
simple
function
illustrates
for
different
types
of
side
effects
and
in
haskó
and
other
function
programming
languages.
Not
it's
not
possible
to
write
any
of
these
types
of
side
effects
in
an
uncontrolled
way
that
aren't
specified
by
the
type
system.
A
Okay,
so
that's
brief,
introduction
to
functional
programming
haskó.
So
it's
a
purely
functional
language
like
I
mentioned,
which
means
all
the
functions
or
mathematical
functions
in
a
language,
it's
not
possible
to
write
an
impure
function.
It's
strongly.
Typed
and
I
won't
go
into
too
much
detail
about
the
algebraic
data
types,
but
it's
basically
just
the
way
of
Haskell
has
four
kind
of
structure
in
the
application
and
have
everything
fit
together
in
the
composable
way,
and
I
will
show
brief
explain
this
brief
function.
A
A
Signature,
the
type
signature
which
tells
you
that
the
function
takes
two
integers
and
then
its
output
value
is
an
integer
and
then
on
the
next
line
you
can
see
what
that
actual
function
is
it
takes
the
two
integers
which
I've
called
x
and
y
and
just
returns
the
sum
of
them
and
then
also
function.
Invocation
in
haskell
also
looks
quite
different
to
what
you
may
be
used
to
from
imperative
languages.
A
So
how
do
these
tie
together?
I've
explained
for
more
verification
and
I've,
also
separately,
explained
functional
programming
and
said
that
they're
important
for
insurance
crappiness.
The
reason
why
these
two
things
are
very
much
connected
and
related
in
this
way
is
because
function.
Programming
language
is
a
very
amenable
to
formal
verification.
A
A
big
reason
for
that
is
because
functional
programming
and
formal
verification
both
have
their
foundation
in
mathematics
and
due
to
every
other
function
in
Haskell
being
mathematical
functions
makes
the
formal
methods
or
the
mathematical
methods
that
are
run
under
the
hood
informal
verification,
a
lot
easy
to
perform
and
haskó
in
particular.
We
just
chose
as
a
is
a
popular
choice,
because
it's
the
purest
mainstream,
functional
programming,
language
and
all
those
logos,
I
showed
you
before
from
the
other
people.
Also
doing
these
things.
The
vast
majority
of
them
are
also
doing
it
with
Haskell.
B
Thanks
Nick,
can
everyone
hear
me?
Okay,
so
for
the
second
half
of
this
talk,
I'm
gonna
be
describing
what
it
takes
to
build
a
new
smart
contracts,
language
in
hyper
ledger
fabric
and
in
particular,
the
work
that
we've
done
in
providing
Haskell
support
in
fabric.
So
just
a
note
in
fabric,
smart
contracts
are
called
chain
code,
so
from
now
on,
all
smart
contracts
equals
chain
code
all
right,
so
just
to
provide
a
bit
of
context.
This
is
a
very
basic
overview
of
the
hyper
edge
of
fabric.
B
Architecture
consists
of
several
application:
clients
that
connect
to
your
network
of
peers.
These
peers
communicate
with
the
chain
code,
which
is
a
user-defined
business
logic
that
dictates
how
the
ledger
is
updated
and
that's
all
coordinated
through
the
PR.
So
the
client
collects
a
series
of
responses
from
the
P
on
a
transaction
proposal
and
then
forwards
the
transactions
onto
the
ordering
service
that
sequences
the
transactions
into
blocks
and
then
sends
the
walks
back
to
the
PR
to
update
the
ledger
so
because
the
chain
code
is
the
gatekeeper
to
the
ledger.
B
B
So
a
bit
more
detail
on
the
peered
chain
code
architecture,
the
PR
and
the
chain
code
run
has
two
separate
processes.
There
are
several
advantages
for
this.
The
first
one
is
that
the
chain
code
contains
user
implemented
code,
so
on
a
trusted
code,
so
there's
failure,
isolation
in
the
case
that
it
crashes
but
important.
It
allows
for
tech,
stock
independence
and
language
independence.
B
It
means
that
we
can
write
the
chain
code
in
a
completely
different
language
than
the
PR
code
is
written
in
and
all
that's
required
is
that
there's
some
standard
of
communication
between
the
two
of
them,
so
the
Perrin
the
chain
code
communicate
via
G
RPC.
They
send
protobuf
messages
chain
code
messages
between
the
two
of
them.
This
is
a
niche
initially
set
up
with
the
register
message
that
sent
from
the
chain
code
shim
and
the
chain
code.
B
Shim
is
like
this
wrapper
that
coordinates
all
of
the
interaction
between
the
PR
and
the
actual
user
implementation
of
the
chain
code.
I
just
want
to
note
here
that
this
architecture
is
specific
for
the
user
chain
code,
there's
also
system
chain
code
in
fabric,
and
that
works
a
little
bit
differently.
B
So
this
is
just
an
example
of
some
communication
that
can
happen
between
the
pier
and
the
chain
code,
so
the
pier
will
send
a
transaction,
their
calls,
an
invoke
on
the
user
user
chain
code
and
if,
as
a
part
of
the
execution
of
that
user
chain
code,
the
chain
code
requires
to
interact
with
the
ledger
in
some
way,
for
example,
to
get
state
from
the
ledger.
It
will
make
a
callback
to
the
PR.
B
So
there
are
actually
a
lot
of
many
more
different
types
of
messages
and
the
one
shown
on
the
previous
slide
all
with
different
functions.
So
the
ones
in
orange
here
are
used
to
set
up
initially
that
pier
chain
code
communication,
so
the
chain
code
will
send
a
register
message
and
the
pier
will
respond
with
a
registered
and
already,
and
this
will
put
the
chain
code
into
a
state
where
it
can
start
to
accept
transactions.
B
The
blue
messages
are
just
the
generic
messages
for
sending
transactions
and
their
responses,
and
then,
if
there's
a
part
of
the
the
execution
of
the
user-defined
chain,
query,
it
requires
to
interact
with
the
ledger
in
some
way.
It'll
send
one
of
these
response
types
in
green.
We
just
have
two
examples
here:
get
state
and
put
state,
but
there
are
actually
many
more
different
types
of
messages
that
the
chain
code
can
send
back
to
the
PR.
B
So
in
this
case,
get
state
put
state
they're,
pretty
self-explanatory,
just
putting
state
to
the
web
job
or
getting
state
from
the
ledger.
So
when
these
run,
when
these
are
called
back
to
the
PR,
the
user
execution
of
the
chain
code
will
actually
pause
and
then
wait
for
a
response
from
the
PR
will
then
continue
in
its
execution
and
then
either
send
a
completed
or
an
error
message.
B
So
the
point
of
this
is
that
what
goes
on
in
the
chain
code
process
is
actually
a
little
bit
more
involved
than
just
simply
running
the
user
code,
because
it
has
to
the
chain
code
has
to
be
a
state
machine.
It
has
to
know
when
it's
in
a
state,
that's
ready
to
accept
transactions,
and
then
it
also
has
to
coordinate
sending
these
calls
back
to
the
peer
and
receiving
responses.
B
So
the
the
component
of
the
chain
code
that
deals
with
all
of
this
complexity
is
called
the
shim
and
it's
actually
made
up
of
a
bunch
of
different
components
within
it.
So
it
has
a
set
up
and
coordination
piece
which
initially
sets
up
that
communication
with
the
PR
there's
a
G
RPC
client
that
sends
and
receives
messages
and
then
a
handler
which
routes
the
messages
to
the
correct
functions.
There's
what's
called
the
chain
code
stub,
which
is
an
interface
it.
B
The
chain
currents
table,
contains
the
entire
context
of
a
transaction
that
is
sent
to
the
chain
code.
This
includes
things
like
the
transaction
ID
and
the
payload
of
the
transaction
proposal,
and
it
also
contains
a
whole
suite
of
methods
that
allow
the
user
to
interact
with
that
context
in
some
way.
B
But
to
do
this
because
the
chain
code
involves
all
of
these
other
things
as
well.
We
had
to
make
some
design
decisions
about
how
this
would
work,
so
he
had
two
main
options.
The
first
one
was
to
leverage
one
of
the
existing
code
bases
out
there,
so
he
uses
much
code,
that's
already
in
existence
as
possible.
B
So
to
do
this
we
would
use
the
Goshen
and
from
that
we
would
take
basically
the
G
RPC
communication
portion
of
that
and
then
because
Haskell
is
such
a
strongly
type
system,
it
would
be
required
that
the
Haskell
part
of
it
would
know
about
all
of
the
type
signatures
of
all
of
the
stub
methods.
So
we
would
have
to
implement
like
that
portion
that
portion
of
it
anyway
and.
B
B
So
the
approach
that
we
took
to
do
this
was
to
use
the
go
code
as
a
base
support
across
into
Haskell,
but
GUI
and
Haskell
used
to
very
different
programming
paradigms.
So
we
had
to
change
the
imperative.
Object-Oriented
go
code
into
pure
functional
equivalents
in
Haskell,
so
this
meant
making
everything
type
safe.
We
had
to
change
all
of
the
statements
to
expressions
we
had
to
get
rid
of
mutable
variables
and
we
needed
to
handle
side-effects
in
a
controlled
manner.
B
So
in
go,
the
mutable
state
is
donna,
terry,
readable,
structs
and
in
Haskell
this
needs
to
be
done
with
state
monads,
so
I'll
just
give
an
example,
quick
example
of
what
this
process
looks
like.
This
is
one
of
the
handler
functions
of
one
of
the
stub
methods
in
go.
You
can
see
immediately
from
the
function
signature
that
there's
it's
not
clear
that
there
are
side-effects
that
are
happening
within
this
this
function,
so
it
takes
a
bunch
of
parameters
and
it
returns
a
byte
array
and
an
error
within
the
function
body.
B
B
All
of
those
statements
that
you
saw
in
the
previous
example
have
been
converted
to
a
single
expression
and
so
having
code
written
in
this
way.
This
pure
way
makes
it
easier
to
reason
about
what
this
function
is
doing.
It
makes
the
code
more
composable
and
more
modular
and
overall,
it
just
makes
the
entire
program
more
on
aníbal
so
of
what
we
have
done
so
far
to
enable
chain
code
Haskell
to
encode
support.
So
far,
we've
done
all
of
the
startup
and
coordination
piece
of
the
shim
all
of
the
G
RPC
communication.
B
So
this
included
the
encoding
and
decoding
of
protobuf
to
Haskell
the
GL
PC
client.
The
message
Hanwha,
which
takes
the
messages,
receives
and
routes
them
to
the
correct
function
in
terms
of
the
chain
code
stub,
we
have
implemented
15
out
of
the
36
messages
methods
so
far
in
terms
of
what's
left,
there's
just
three
core
functions,
and
these
are
the
state
iterator
functions
like
get
state
by
range,
so
that
21
methods
that
are
left
most
of
those
are
just
derivatives
of
these
three
core
functions.
B
So
the
shim
is
completely
functional.
It's
working,
so
we
can
start
writing
some
user-defined
chain
code.
So
we've
we've
done
that
we've
recreated
one
of
the
common
examples.
It's
used
in
fabric,
which
is
the
fog
car
example.
It
trucks,
car
ownership
for
the
blockchain,
so
I'll
show
you
what
one
of
the
methods
from
the
third
car
example
looks
like
in
Haskell.
So
this
is
a
change
car
or
in
a
function.
B
Again,
you
can
see
from
the
function
signature
that
it
returns
an
I/o,
so
there's
side
effects
happening
in
here
on
line
four,
you
can
see
that
it
makes
a
call
back
to
the
peer
to
get
state
from
the
ledger
when
it
receives
a
response.
I
would
then
create
a
new
car
instance
with
the
new
owner
and
then
line
12.
You
can
see
that
puts
that
state
back
to
the
ledger.
B
So
this
is
an
example
of
a
function
that
makes
multiple
calls
back
to
the
PR
and
it's
all
all
done
in
a
single
expression
and
in
a
pure
way.
So
from
this
you
might
be
wondering
when
you
can
get
started.
Writing
your
own
Haskell
chain
code
and
I'm
pleased
to
say
that
all
of
our
work
is
now
open
source.
B
So
just
know
that
this
is
experimental
at
this
stage.
It's
not
feature
complete,
but
this
repo
contains
documentation
on
how
to
get
started,
as
well
as
some
simple
examples
of
chain
code.
So
we
encourage
everyone
to
please
fork
it
test
it
out.
Try
writing
your
own
chain
code
in
Haskell.
If
you
find
issues
raise
them,
if
you
want
to
contribute,
you're
feel
free
to
open
a
pull
request.
B
B
Yeah,
so
in
conclusion,
we
hope
that
we've
convinced
you
that
block
chains
are
critical
systems
and
therefore
it's
vital
that
the
smart
contracts
are
correct.
Formal
verification
is
the
current
state
of
the
art
to
ensure
code
correctness
and
functional
programming
provides
a
good
foundation
for
formal
verification
because
of
their
shared
roots
in
mathematics.
So
we've
implemented
support
for
Haskell
chain
code
in
fabric,
and
we
believe
this
is
the
first
step
to
being
able
to
provide
formally
verifiable
chain
code.
B
So
we're
not
done
yet.
As
I
mentioned,
we
still
need
to
finish
implementation
of
the
stub
function,
so
three
core
functions
left
to
go.
We
need
to
add
support
for
concurrency
in
the
chain
code
and
finally,
we
need
to
implement
further
verification
of
both
the
Haskell
shim
and
also
enable
formal
verification
of
the
user-defined
chain
code.
We'd
also,
eventually
like
to
get
this
get
Haskell
officially
accepted
as
one
of
the
fabric
languages,
smart
contract
languages.
B
B
A
So
JavaScript
Java
and
go
or
all
general
purpose
languages,
and
we
did
consider
like
a
DSL
like
you're
asking
about,
but
we
figured
if
we
kind
of
added
support
in
that
way
and
made
a
specific
to
yourself
a
domain
like
damn
holes
for
the
financial
services
area.
It
wouldn't
really
match
the
way
the
support
of
the
other
three
languages
are
supplied
and
we
thought
in
terms
of
getting
people
on
boarded
and
using
a
language.
We
wanted
to
kind
of
make
it
as
similar
to
the
existing
ones
as
possible
when
just
have
it
more
general-purpose.
B
So
the
state
is
stored
in
the
actual
ledger,
so
the
chain
code
itself
is
stateless.
Apart
from
the
fact
that
it
it
records
whether
it's
ready
just
receive
transactions.
But
apart
from
that
in
terms
of
all
of
the
transaction
proposals
that
come
through
that
chain
code
process,
none
of
that
is
stored
locally.
So
the
chain
code
itself,
the
Haskell
portion,
is
stateless
and
then
all
of
the
state
is
sent
to
the
PR
through
the
PA
to
the
ledger.
B
A
B
C
B
Don't
think
we
haven't
done
any
performance
tests
of
the
way
that
Haskell
will
run.
We
still
need
to
implement
the
concurrency
portion
of
the
Haskell,
so
I
think
that
time
will
tell
the
Haskell
has
a
very
elegant
way
of
dealing
with
concurrency.
So
we're
hopeful
that
when
we
do
implement
the
concurrency
in
Haskell
that
it
will
actually
be
able
to
process
transactions
faster,
but
we
can't
tell
you
just
yet
well
let
you
know.
A
A
Not
not
at
this
point
now
so,
like
I,
said
we're
we're
still
kind
of
building
the
foundation
of
like
flushing
out
the
rest
of
the
house
girl
support.
First
and
then
we
have
some
ideas
of
different
like
because
there's
various
ways
to
perform
formal
verification
and
Haskell
in
general
that
designed
by
contract
that
I
presented
is
kind
of
the
main
approach
for
formally
verifying
functions.
A
So
we'll
probably
be
doing
some
approach
like
that,
but
regarding
details
we
haven't
it
chosen
the
exact
approach
we
want
to
take
with
that
and
therefore
don't
haven't,
come
up
with
best
practices
design
patterns.
But
there
are
so
I
mentioned.
The
DAO
attack
is
a
reentry
attack
and
there
are
some
other
well-known
like
types
of
attacks
that
can
happen
like
overflow
and
underflow,
and
things
like
that
and
just
the
general
like
a
good
design
by
contract
form
or
very
formally
specified
specification.
I
guess
would
protect
you
from
all
of
those
as
well.
A
A
See
you
do
need
to
have
some
expertise
and
knowledge
and
for
verification
to
know
what
what
and
how
you
need
to
specify
a
send
piece
of
code.
So
it
does
require
some
ups
going
I
guess
for
someone
to
be
out
for
the
FBI
a
programmer
to
be
able
to
start
for
me
verifying
code,
there's
a
bit
of
a
step
there
about,
hopefully
with
examples
and
more
people
getting
on
board
like
Accord
that
that
process
will
become
easy.
A
So
we
haven't
got
to
the
step
of
actually
doing
the
formal
verification,
yet
so,
like
Alison,
presented
with
building
out
the
foundation
and
having
this
whole
house
girl
support
because
house
girls
a
very
minimal
language
for
the
formal
verification,
but
we're
not
quite
at
the
point
of
actually
having
that.
Well,
we're
still
completing
the
actual
shim,
and
when
that
is
done,
then
we'll
start
exploring
the
different
ways
of
doing
from
location.
But
there,
the
user
chain
code
example
that
Alison
showed
if
the
fab
car
that
is
not
being
formally
verified.