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