Lean supports coinduction, which allows you to write programs which run indefinitely. This even allows you to embed Turing-completeness, it just has to be declared as potentially non-terminating up-front.
This is a common property for proof-oriented languages. Coq shares this property for instance, and you can write an optimizing C compiler in Coq: https://github.com/AbsInt/CompCert .
Why is that? If a proof can not be found isn't that like not halting, since the space of all theorems can never be exhaustively checked? And we know there are things which can not be proven.
>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)
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.
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.
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.
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.
You can stick "partial" in front of a function definition if you want to live dangerously. I've had to do that in a couple of spots in my Advent of Code stuff.
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.
Yes, that is incorrect. If you write `partial def foo : Nat := foo + 1` it will be accepted, but `def foo : Nat := foo + 1` is not. So while lean checks that functions terminate by default, it is possible to define and run programs containing general recursion. This is subject to some restrictions though:
* You can't unfold the definition to try to prove `foo = foo + 1` (which is of course false for any natural number), it is an "opaque" definition and its value for specification purposes is essentially arbitrary and does not need to match the definition.
* Even then there is a possibility of proving false things as in `partial def loop : False := loop`, so to prevent inconsistency the target type (`Nat` in the previous example, `False` in this one) must be inhabited (proved automatically by the typeclass machinery). So it would reject the `loop` example but not `foo`.
You can only write programs that will halt in it.
https://leanprover.github.io/about/