I've been trying to teach myself Coq, one of the formal provers mentioned in the article, so I'll try to explain how Coq works, and I'll send you to another web

I've been trying to teach myself Coq, one of the formal provers mentioned in the article, so I'll try to explain how Coq works, and I'll send you to another website with a tutorial instead of trying to explain how to use it. In Coq you may define a set in terms of constructors of that set, for instance the set of natural numbers is: Inductive nat : Set := | O : nat | S : nat -> nat which is saying that natural numbers may be made in one of two ways, you may take the constructor O at any time, or you may take the constructor S which takes a natural number. O is zero, and S is "successor", meaning +1, so that S(O) is 1 and S(S(S(O))) is 3. The language is dependently typed, which means that expressions may be used as types. If you'd like to construct an "int" in C you may give an example such as "4". If you'd like to construct a value with "x < y" type in Coq, you must provide an example, either building it through theorems. As a programmer, it's a process similar to looking through an API manual, you know you have an object of one type and you know the type of the object you need, and you're trying to find the path that gets you one from the other. Often times the function you need won't already exist and you'll have to define a new function in code, then use that function in your proof. For flavour, here's what that looks like in Coq. This is my attempt at defining natural numbers as Church Numerals, then defining multiplication on them: Definition nat := ∀ X : Type, (X → X) → X → X. Definition mult (n m : nat) : nat := fun (X : Type) (f : X → X) (x : X) => n X (m X f) x. If you can build up value 'z' whose type is "x < y" then it's important that when you use it, it still be true that x is less than y later. For this reason, Coq is a functional programming language without mutability. Dependent types have implications across the language. For instance you could have a record (like a C struct) whose three members are a numerator, a denominator, and a proof that the denominator != 0. Another cool thing is that it lets you write more expressive APIs such as a "pop()" function on a queue. In most languages your options are to make it undefined behaviour to pop an empty queue, or return a result type that may contain an error, or use exceptions if your language supports them. In Coq, you may define pop() as a function which takes a parameter whose type is a proof that the queue is not empty when called. (Due to Coq being pure functional, pop() also returns the whole post-pop queue.) When proving, you have the goal to prove some statement, and some hypotheses that are known true in your current state. You may apply any theorems previously proven to transform your goal or hypothesis. Generally this means breaking the problem down into stages, such as splitting on 'and' and 'or', or performing induction on a variable. This proofing language is different from the programming language. The best tutorial I've found online is for Lean prover, not Coq, but the concept is the same. (Indeed, other than lean using "rw" where Coq uses "rewrite", I can't recall any differences at all): https://news.ycombinator.com/item?id=22801607 https://news.ycombinator.com/item?id=22801607 The main problem I have with Coq is its lack of automation. If I understand the history, that's a bit of an ironic statement because Coq's main feature was its automation. The statements to "rewrite based on this theorem" or "split on 'and' and form two goals" are tactics, and Coq allows you to write your own tactics. There's no need for tactics to be proven correct, they can be full of bugs, either they show a path to produce a value with the right type in which case you have a proof, or they do not. My problem is that the Coq developers seem to share an opinion that the user is a mathematician who has considered the problem, developed a proof, attempted to formalize the proof on their own paper, and is as a last step entering their formalized proof into Coq. As a non-mathematician, I have done none of those things. I understand that they avoid doing things that may consume CPU time like trying every combination for a variable, but the "auto" tactic won't try 'true' and 'false' for a single boolean variable. The one last step is that you can "extract" running code from Coq proofs. I've never done this myself, so I can't speak to it, but the idea is that you want to remove the concern that the code you've proven isn't the code you actually run. Coq can emit OCaml or Haskell.