Victor MaiaThoughts 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…Aug 11, 20202Aug 11, 20202
Victor MaiaFunext follows from Self-TypesA proof of function extensionality in FormalityMay 27, 2020May 27, 2020
Victor MaiaFunext from self?Can we derive function extensionality from self types only?May 6, 20201May 6, 20201
Victor MaiaThe 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…Feb 14, 2020Feb 14, 2020
Victor MaiaCompiling Formality to the EVMCost of a beta-reduction: ~200 gasDec 29, 20191Dec 29, 20191
Victor MaiaCalling a function a googol times.Yes, this is about optimal reductions!Aug 28, 20191Aug 28, 20191
Victor MaiaIntroduction to Formality (Part 1)Why it exists, installation, simple types, programs and proofsApr 22, 2019Apr 22, 2019
Victor MaiaTowards 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…Jan 26, 20193Jan 26, 20193
Victor MaiaAbout 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.Oct 3, 20181Oct 3, 20181
Victor MaiaUpdates on Ethereum’s Moon ProjectFormal proofs, parallel FVM and ideas for mass adoptionAug 29, 20185Aug 29, 20185