# Grantee Exposé Lightning Talk 1 - Formality: An efficient proof language by John Burnham (Devcon5)

- Channel: [Devcon](https://streameth.org/devcon)
- Date: 2020-10-09
- Duration: 10:20
- Topics: blockchain, smart contracts, distributed ledger, ethereum
- Watch: https://streameth.org/watch/yt-3XUKQX4nN8w
- YouTube: https://www.youtube.com/watch?v=3XUKQX4nN8w

## 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/5/grantee-expose-lightning-talk-1-formality-an-efficient-proof-language

Formality is a dependently-typed functional programming language similar to Agda that compiles to a non-garbage-collected, parallel runtime based on interaction combinators and Lamping's optimal reduction algorithm. The language is suitable both as a formal proof language as well as a fast low-level systems language, which allows it to be used to write verifiably secure software at every level of the stack, from hardware drivers to smart contracts and everything in between. Formal proofs are of particular interest for smart contracts applications, given that they often have large amounts of capital depending on the safety of relatively small code bases. 

Speaker(s): John Burnham
Skill level: Intermediate
Track: Security
Keywords: programming, runtime, proof, security, general

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 5 was held in Osaka, Japan on Oct 8 - 11, 2019.
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

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]