Proofs about Programs

While I'm not deeply familiar with these, Lean's documentation opens with:

> ... interactive theorem proving focuses on the "verification" aspect of theorem proving, requiring that every claim is supported by a proof in a suitable axiomatic foundation. This sets a very high standard: every rule of inference and every step of a calculation has to be justified by appealing to prior definitions and theorems, all the way down to basic axioms and rules. In fact, most such systems provide fully elaborated "proof objects" that can be communicated to other systems and checked independently. Constructing such proofs typically requires much more input and interaction from users, but it allows you to obtain deeper and more complex proofs.

https://leanprover.github.io/theorem_proving_in_lean4/introd...

Which sounds very much like a type system to me. You can build complex statements out of finitely many previously-proven statements. The system may try to help you bridge the gap, but as I understand it, ultimately it's up to the user/programmer to find the proof that something will halt.

Proof systems are for doing mathematics. A function in these is a mathematical function and not a function in the programming sense of the word. For a mathematical function 'this computes forever' is not an acceptable outcome.

>If a proof can not be found isn't that like not halting, since the space of all theorems can never be exhaustively checked?

That's correct, and the consequence is that Coq will reject some valid recursive functions that always terminate. You can't describe the Collatz function in Coq and then ask the compiler if it terminates or not, for example. The compiler will reject the function, but it may still terminate - we don't know.

The general reason for this is that Coq allows you to write recursive proofs (such as the induction in the article), and these recursive proofs need to have limited power - otherwise the proof system becomes inconsistent and it's possible to prove any statement. Since Coq proofs are just programs, if you could write a recursive non-terminating function, you could write such a function that lets you construct ill-founded proofs e.g.

    (* Non-terminating Coq function *)
    fix : (A -> A) -> A
    fix f := f (fix f)
    
    (* Use of that function as a Coq proof building tool *)
    my_false_statement : ⊥
    my_false_statement := fix (fun x => x)

With a constructive logic like the one with Coq, you can use functions as proofs of theorems. Briefly, a function is a constructive proof that you can construct an object of the output type from objects of the input type. This means that you can see types as theorems and functions as proofs of those theorems. But in order to be able to prove useful theorem, you want to enforce that every function does really return an output in all situation.

I think you should rather ask GP "How do you know that?". The link to the about page of Lean doesn't back up the claim that you can only write programs that halt.

And indeed, you can write programs that do not halt. You just have to explicitly tell Lean that you want to do that.