hi everyone good morning my name is Sean
and I'm working on the formality proof
language with my co-founder Victor Maya
what's a proof language so let's do a
quick refresher on type systems here's
some pseudocode representing an array
indexing function in an untyped language
I take an index and an array and I try
to get whatever's inside the array at
that index get 1 is bar because array
indices start at 0 and get 2 is bats
here's a riddle
if get 1 is bar and get 2 is baz what's
get 1.5 better question what should get
1.5 be a runtime error indexing an array
with a non integer makes no sense
because an untyped language but a none
type language lets you shoot yourself in
the foot and make a bad function call
and this only fails during execution ie
when your codes running and can affect
the world around it runtime errors are
tough because sometimes they do nothing
and sometimes they cause your spacecraft
to perform a rapid unscheduled
disassembly your codes runtime could be
in five minutes on your laptop or it
could be 30 years for now on devices
that don't even exist yet you don't know
its runtime by adding some types we can
get the compiler to complain hey fix
your code you can't have an index that's
not an integer this error might look
deceptively similar the previous one but
there's one crucial difference it occurs
before your code runs that is before it
can do any damage but simple types are
kind of inflexible this function only
works for arrays that contain integers
if we want different array contents in a
simply type language we need a
copy/paste lots of boilerplate lots of
languages try to solve this with things
like interfaces but there's a better way
polymorphism allows us to have a type
parameter a that can get filled with int
or string or any type that we like this
is really useful and most type languages
stop there but this still doesn't
prevent all runtime errors we could call
get with a really large index and cause
an out-of-bounds runtime error some
languages don't even error they just
dump the contents of memory and that's
probably worse but for what the compiler
to warn us if our index is bigger than
our
we're gonna need types that depend not
only on other types but on normal values
here we have a type type level number n
that tells the compiler how long the
array is just like we have a type
parameter a that tells us what's in the
array n is a type level value that lets
us enforce that our index has to be
between 0 and n minus 1 the values
independent types don't have to be
constants they can be the results of
computations this lets us constrain the
function so much that we can often guess
what the implementation has to be just
from its shape kind of like a game of
who's that Pokemon but with types in
this case we have a function that
receives a number n and returns an array
of prime numbers that have multiplied
together equal n Karen can anyone guess
what this has to be it's factorize the
cool thing is nothing other than the
correct factorization implementation
will pass the type checker that the
Fibonacci sequence would be a type error
because the products wouldn't sum to it
to the number let's play again given an
array X's return an array wise with the
same elements but in ascending order
what does this function have to be sort
anything else is a type error those such
that to check statically which means
that you will not go to space today
becomes my code is broken and I don't
know why which is great because compile
time is when you the programmer are in
the process of fixing your code this is
really nice for immutable block chains
where a runtime error means my code is
broken no one can get their money out
and I can't fix it because I deployed my
code to an immutable platform but
dependent types are useful for so much
more if we can do arbitrary type level
computation we can use our type system
to declare any number of any combination
of properties we want and then if we
write code that validly checks as those
properties we've built a constructive
executable proof of the theorem that
type represents this is the curry Howard
isomorphism and by favorite isomorphism
formal logic and software development
are actually the same activity it's just
not obvious because the usual syntax is
very different most math syntax forces
you to do the execution manually and
most code syntax forces you to keep
track of type information manually our
goal with formality is to have a
language that's really really good for
both software development and for
exploring mathematics
we want to make a programming language
as accessible as Python and a proof
language as powerful as Agda one that's
safe fast simple and portable we still
have a long way to meet that goal but
we've made great progress in the past
year here's all the type signatures we
just went over but informality syntax
instead instead of pseudocode and here's
how we declare datatypes and how we take
the tail of a list the cool thing here
is that unlike other proof languages
like or Agda our data types aren't
built in to the theory they're actually
just a syntax sugar for lambda functions
this this code looks a little scary from
a user perspective which is why we built
the syntax trigger over the past year
but it's actually a lot simpler to
implement and our runtime is only about
400 lines long and our core language
theory is only about 1500 we think it's
really important for portability and
decentralization to have a language
that's small enough that people can
implement it or at least understand it
themselves here's the clean syntax again
you know now that you know the laminin
codings look like let's talk about
performance a language is great for
writing practical software has to be
fast while formalities runtime is still
immature the language has a lot of
features that we think will make it very
fast in the long term interaction that's
is a runtime model and I think it
deserves its own talk since they allow
some really crazy optimizations like
optimal sharing runtime Fusion and
here's our nice illustration of what
like the reduction actually looks like
and you can see the conversion from a
lambda X term to a graph and then back
for code with higher-order lots of
higher-order functions formalities
extremely fast right now but there's
still substantial overhead which makes
us only moderately fast on average at
the moment we think in future our
interaction that model will pay a lot of
dividends here performance is really
critical to us for getting people to
adopt formality and using it to build
lots of great software one interesting
thing about these benchmarks is that if
instead I call the function not ten to
the hundred times but ten to the hundred
thousand it still only takes like 12
seconds which is you know way better
than I think pretty much any other
language that I've used unless you do
like crazy optimizations
here's why proofs matter here's a sample
of some costly issues that have happened
at different parts of the stack that
perhaps could have benefited from proofs
and type safety heartbleed that's just
an out of bounds indexing error now
proofs aren't a silver bullet because
all these issues are really complicated
but if proofs can reduce the severity or
incidence of these kinds of errors even
just a little bit at the margin I think
it's worth exploring and in black Shang
I think it's especially especially
relevant because the ratio between code
complexity and code value is so extreme
here I just counted the lines in you
know some popular projects you know ba
tu SDC and you know a lot of projects
are running at about a million line a
million dollars of capital per lines of
code so I think it's really important
that if you're writing projects like
that it's you should put a little extra
effort in trying to make sure that the
lines of code are actually the correct
lines of code one criticism of proofs is
that they pass responsibility for
correctness to the specification rather
than the implementation and you still
have to audit it and that's completely
true like it doesn't this proofs don't
solve having to actually think about
your code and reason reason that is
correct and if you're type spec is bad
then you'd proofs don't help you but
type specifications can be much simpler
than the code they're typing and at
worst act like a compiler check
documentation here's a little snippet
from our er C 20 implementation and you
can see that like if we that we have
this type specification that says I have
a transfer function I have the approvals
have to be in an old state that has to
be removed from a new state and it has
to obey a double entry bookkeeping
environment you don't even need to see
the implementation to know that if it
type checks those properties that it's
going to long as the compilers valid
that it's going to be safe according to
those properties the vision is to have
formality be a language that can add
type safety at every layer of the stack
having the same language every matter
means that you can use the same types
everywhere with minimal friction and
this is what's awesome about having a
400 line language implementation we can
have the same language infrastructure
running inside a web app smart contract
server editor plug-in or our test suite
our next big priority now that the
language is pretty stable is to write
the compilers that will let us deploy
formality smart
contracts and to continue maturing the
library's tools and Docs to make that a
really great user experience after that
implementing formality in itself will
improve portability even further and
we're gonna see how fast we can push the
existing C implementation the two
projects after that are going to be our
package management infrastructure and
putting the formality type checker on an
aetherium contract that enables us to
build a completely trustless marketplace
for code and proofs you can submit a
formality type to a contract along with
a bounty for the first valid
implementation of that type and then
anyone in the world can claim the bounty
just by submitting the code no human
interaction required if it passes the
type checker you get paid and that's
formality Thanks happy to take any
questions I don't think I have any time
okay
[Applause]