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?
"That’s because Lean only lets you write functions that halt. "
Is that incorrect?
* 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`.