Rice’s Theorem just proves that there’s no algorithm that determines if property B holds for all programs, this doesn’t stop you from proving the same for specific programs. (For some intuition, it’s clearly possible to write programs that provably halt—like a program consisting of “return 0” and nothing else—even though the halting problem is insoluble in general)
Expanding on this, there are several programming languages (Idris, Coq, etc.) whose type system ensures that every program that type checks will halt when it’s run. One way to view a type system is as an automated search for a proof that your program is well-typed (and a type error is a counter-example). In a language like Idris or Coq, a program being well-typed implies that it halts. So machine generated proofs that programs halt aren’t just theoretically possible, they’re used extensively by some languages.
Rice’s Theorem just proves that there’s no algorithm that determines if property B holds for all programs, this doesn’t stop you from proving the same for specific programs. (For some intuition, it’s clearly possible to write programs that provably halt—like a program consisting of “return 0” and nothing else—even though the halting problem is insoluble in general)
Expanding on this, there are several programming languages (Idris, Coq, etc.) whose type system ensures that every program that type checks will halt when it’s run. One way to view a type system is as an automated search for a proof that your program is well-typed (and a type error is a counter-example). In a language like Idris or Coq, a program being well-typed implies that it halts. So machine generated proofs that programs halt aren’t just theoretically possible, they’re used extensively by some languages.