> But you wouldn't write a program that depended on a theorem that wasn't proven, no? I mean often the only mathematically hard parts of a given program are in

> But you wouldn't write a program that depended on a theorem that wasn't proven, no? I mean often the only mathematically hard parts of a given program are in the libraries it uses - which could ship with their own proofs. Proofs for nontrivial programs quickly get into undecidable areas in terms of proof automation. You might have relevant theorems lying around but how you combine them to create your proof is an undecidable problem. As an example, if you have integer theorem statement where you can only multiply variables by constants (e.g. x * 5 + y * 2 ... = x * 2 + ...) there's an algorithm that can always find a proof. If you relax this restriction, no such algorithm does or can exist that will always find a proof. > Doesn't the structure of the code tell you how to structure the proof though? Like, if you've written code that appends to a list by appending a single element and recursing, the way you prove it correct is to prove that it appends a single element and that it recurses correctly. Usually you'd use inductive proofs to write those kinds of proofs and the induction scheme you use would follow the way recursion is done in the program. That doesn't mean the gaps in the proofs (e.g. base and step case) are trivial though. > If you've written something that's supposed to be a sorting algorithm and the code rearranges the elements of a list, why is it that you believe this particular rearrangement of the elements is a correct sort? Isn't the answer to that question your proof of correctness? The jump from a rough intuition about why something is provable to a proof is much larger than you'd think. I'd recommend following a tutorial on Coq. It's worthwhile even if you don't go beyond a quick look so you can appreciate the almost vertical learning curve if you're not well versed in maths and logic (which most programmers aren't) and how proving simple facts rigorously (e.g. "list_reverse (list_reverse x) = x") requires a lot of effort.