# Introducing Formality by Victor Maia & Leonardo Souza (Devcon4)

- Channel: [Devcon](https://streameth.org/devcon)
- Date: 2019-10-09
- Duration: 10:55
- Topics: blockchain, smart contracts, distributed ledger, Science & Technology
- Watch: https://streameth.org/watch/yt-0fg1QbeeqNU
- YouTube: https://www.youtube.com/watch?v=0fg1QbeeqNU

## Description

Visit the https://archive.devcon.org/ to gain access to the entire library of Devcon talks with the ease of filtering, playlists, personalized suggestions, decentralized access on IPFS and more.
https://archive.devcon.org/archive/watch/4/introducing-formality

In 2017, I presented the ideas behind the Moon Project, which aims to create a blazingly fast and secure decentralized browser for DApps. In this talk, I'll highlight advancements towards this goal, highlighting Formality, a massively parallel programming language featuring formal proofs and smart contracts, and the FVM, a decentralized virtual machine dedicated to running functional programs with much lower gas costs using the so-called Abstract Algorithm.

Speaker(s): Victor Maia, Leonardo Souza
Skill level: Intermediate
Track: Security
Keywords: formality, language, programming

Follow us: https://twitter.com/efdevcon, https://twitter.com/ethereum
Learn more about devcon: https://www.devcon.org/
Learn more about ethereum: https://ethereum.org/ 

Devcon is the Ethereum conference for developers, researchers, thinkers, and makers. 
Devcon 4 was held in Prague, Czech Republic on Oct 30 - Nov 2, 2018.
Devcon is organized and presented by the Ethereum Foundation, with the support of our sponsors. To find out more, please visit https://ethereum.foundation/

## Transcript

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