proofs

If you're already familiar with a functional programming language like Haskell or OCaml, you have the background to work through my Coq tutorial here: https://github.com/stepchowfun/proofs/tree/main/proofs/Tutor... My goal with this tutorial was to introduce the core aspects of the language (dependent types, tactics, etc.) from first principles. If you're fascinated by proof assistants like Coq or Lean and want to understand how to use them, this tutorial is written for you. Any feedback is appreciated!

It's always a pleasant surprise to see people using Coq and other formal verification technology to build confidence in their ideas and algorithms. We need to stop producing buggy software! If this article gave you a thirst for interactive theorem proving and you want to learn it from the ground up, I've recently written a Coq tutorial [1] which covers topics like programming with dependent types, writing proofs as data, and extracting verified code. That repository also contains a handy tactic called `eMagic` [2] (a variant of another useful tactic called `magic`) which can automatically prove the theorem from the article. [1] https://github.com/stepchowfun/proofs/tree/main/proofs/Tutor... [2] https://github.com/stepchowfun/proofs/blob/56438c9752c414560...

Coq is so much fun. It makes writing proofs feel like playing a video game. I've just finished writing a Coq tutorial [1] that is aimed at programmers (rather than, say, computer scientists). It covers topics like programming with dependent types, writing proofs as data, universes & other type theory stuff, and extracting verified code—with exercises. [1] https://github.com/stepchowfun/proofs/tree/main/proofs/Tutor...

I highly recommend just downloading and playing with a language based on type theory, such as Coq/Lean/Agda. I know Coq well, so I can recommend Software Foundations and Certified Programming with Dependent Types. Write some simple proofs in one of those languages; for example you could try proving that addition of natural numbers is associative and commutative. At some point, it will start to click and you will feel like every other programming language you've ever used before is severely underpowered for not having dependent types. If you don't have experience with typed functional programming (e.g., Haskell/OCaml/SML), you will probably want to start learning one of those languages first. These languages won't really teach you type theory (at least, not the powerful kind of type theory that lets you do mathematics), but they will help