[7ewkVE6jJquN7e3]

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.

[galaxyLogic]

Just to be clear on https://busy-beavers.tigyog.app/proofs-about-programs if you can locate the section "Once more, in Lean", it says:

"That’s because Lean only lets you write functions that halt. "

Is that incorrect?

[digama0]

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`.