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

Fri, Oct 2, 2020, 12:00 AM

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/