in the same way computers the internet
and smartphones gave us new ways to
interactive software we believe a new
era of crypto browsers is about to begin
the moon project is our attempt at
finding the best user experience for a
children okay okay
this is example tap on moon browser the
browser is just looks like a normal web
browser but it has three major
differences there which are represented
by those three buttons on the upper
right corner first instead of normal
accounts and passwords everything is
based on crypto signatures right so
first like a mist you can just store
your assets here you can manage them
without a bank and but really nothing of
this is no so let's move on yes this is
not really new because miss does that
alright but imagine if you could fork an
application in a single click not just
the front end not just a interface not
just a video the entire company in a
single click imagine if you called fork
YouTube in a single click that's what
the fork button above there does and
that's one of the difference we have so
now if we are outside if we want to
store real money on apps then we need
something else than JavaScript like
languages which are not enough anymore
really the tabs need a formal
specification something that tells us
that states in cold actually everything
that promises to do then if we ask the
browser to check on the formal
specification the mathematical proof of
that specification we can be sure that
the program does what we expect
in other words by just checking the
first the first line is there we could
have avoided the entire deal instead
it's one line that if someone just read
it it could have avoided everything that
happened two years ago on the Dow fiasco
so this was our vision but there was a
problem
those are some of the most popular proof
languages in the market for many reasons
some simple or the very complex none of
them had everything we needed like we
wanted those one of those languages
should be the JavaScript of our browser
but none of them had had at all some of
them almost did it
but there's one thing none of them had
performance there was no language in the
world that had high level that what was
high level had former proofs and was
first enough was fast enough for us so
if you wanted to compile some of those
language to to the idiom the cost of
course of doing that would be very
expensive you guys with a lot of a lot
of money yet in our transaction and then
it would not be practical yeah
the bad news is that we had to stop our
browser development to focus on making
our own language the good news is that
it is awesome so better than our
presentation so that con today the moon
team proudly presents you formality
formality is a high-level functional
programming language that features
formal proofs that is not garbage
collected and that targets DVM and GPU
the only language in the world that does
that it's simple enough for you to
implement it yourself in other words if
you don't trust our shaker you can do
you can implement for mulcher self and
it has the potential to be very fast
which we will explain some thank you
well fermented programs have two
building blocks one inductive data data
types
they represent data like natural numbers
like vector vectors equality
certificates and two functions they
represent computations and proofs so
some things like doubling in a number
like fetching the first the first
element of a vector or proving the
symmetry of equality but that's pretty
standard on proof language so we won't
spend a lot of time this so let's move
on to the fun part that's how fast
format is how fast it can be please
check this code it's very simple it does
three things first it creates an array
with 100 zeros then it used the map
function to increment every number by 1
and million times and then it outputs
the result it's very simple how long it
takes to run this code in different
levels as you can see for mulch bits
every other language and the difference
is huge
this is not a compile time optimization
is not some clever trick this is
actually what happens when we want very
high level code of a mallet there is no
other language in the world capable of
optimizing functional high level code
like it if you don't believe me please
check our benchmarks on the link below
where we also explain why that's the
case but that's not a whole history yeah
let's have a look at this other example
this also does three things
the first thing it creates a linkedlist
of bits then just flips them over and
over about a million times and then it
prints out the result
how fast can this execute as we see here
formalities now slower than the rest it
happens because the code is too
low-level so it can't be really
optimized formality is to an interpreted
language so it can't compete and raw
performance with other major compilers
but that's okay the potential is here
and you'll see why in the next example
so this is the same code this is the
same thing now running on the GPU so yes
that's true you can take any formality
program and run it in thousands of
course in parallel with no program
effort at all and we can get real speed
ups with that so this is something that
also no other functional language in the
world is capable of doing you can't
compile Hosko it is anything that you
think to the GPU and formality can do
that we believe that with a sufficiently
major compiler we could beat those
language so how how can a high-level
language like four miles have no garbage
collection how can it often be fast on
the Haskell how can it ship the targets
the VM or even the GPU memories those
are the four axes of formality linear
types like rows values can only exist in
one place at the same time making
garbage collection unnecessary memory is
freed when values go out of scope simple
as that these clones
unlike rust values can be cloned with no
cost make linearity much less painful as
we don't need to borrow values so that's
possible because copies are made lazily
on better optimality functions are
reduced optimally this allows an insane
amount of rot and fusion to happen
breaking down bloated high-level code
into small lightweight computations if a
strong confluency evaluation is shrunken
fluently confluent so the order of
execution doesn't change the required
work to complete the computation this
allows reductions to take place in any
order even in parallel so all those
things allows for mallet should be
compiled to a new model of computation
called interaction combinators which
combines the best aspects of Turing
machines and the lambda calculus that's
what allows us to run and to run on the
GPU to compile to JVM and everything
else we presented so far if that sounds
fun to you and they really think that's
very fun please check the link below
where we explain this model a little bit
better and that's it formality turns
scientific scientific breakthroughs into
a real-world language so with this we
are closer to building the moon browser
as we are originally envisioned
formality is not officially released yet
there's a lot of boring work to do but
the fundamental parts are done and you
can check it today on github ok so just
a Lansing there's a brilliant researcher
called ørestad that created a type
theory that fits in a single slide it's
that thing you are seeing here that
theory is not only very powerful more
powerful than angular and eateries and
is about another language but it's also
much much simpler and sadly we don't
have enough time to explain how this
work today but this is what will be used
by for mileage to ensure mathematical
consistence which is which is something
very hard to do in proof language and we
actually gave a bread for our stop to
make this possible so we are very
thankful to him for that and that's it
thank you very much sorry about Java
[Applause]
you