Victor Maia·Aug 11, 2020Thoughts about FormalityI’m writing this article to talk about the proof and programming language I developed, Formality, some bits of its history, why it exists…A response icon2A response icon2
Victor Maia·May 27, 2020Funext follows from Self-TypesA proof of function extensionality in Formality
Victor Maia·May 6, 2020Funext from self?Can we derive function extensionality from self types only?A response icon1A response icon1
Victor Maia·Feb 14, 2020The refreshing simplicity of compiling Formality to… anythingFormality is a new programming language featuring theorem proving that, unlike most in the category, is designed to have a familiar syntax…
Victor Maia·Dec 29, 2019Compiling Formality to the EVMCost of a beta-reduction: ~200 gasA response icon1A response icon1
Victor Maia·Aug 28, 2019Calling a function a googol times.Yes, this is about optimal reductions!A response icon1A response icon1
Victor Maia·Apr 22, 2019Introduction to Formality (Part 1)Why it exists, installation, simple types, programs and proofs
Victor Maia·Jan 26, 2019Towards a simple theorem proverSince a long time ago, I’ve been looking for a simple theorem prover: a small (say, ~1000 LOC) programming language capable of expressing…A response icon3A response icon3
Victor Maia·Oct 3, 2018About induction on the Calculus of ConstructionsThis post is meant to be a summary of my current understanding of this matter, and to present some naive ideas that are probably nonsense.A response icon1A response icon1
Victor Maia·Aug 29, 2018Updates on Ethereum’s Moon ProjectFormal proofs, parallel FVM and ideas for mass adoptionA response icon5A response icon5
