I was thinking about proofs and ran into an interesting observation. So proofs are equivalent to programs via the Curry-Howard Isomorphism, and circular proofs correspond to infinite recursion. But we know from the halting problem that in general testing whether an arbitrary program recurses forever is undecidable. By Curry-Howard, does that mean there is no "proof checker" that can determine if a proof uses circular reasoning?
I've always thought that proofs are supposed to be composed of easily-checkable steps (which correspond to applications of inference rules), and checking all the steps gives you confidence that the conclusion follows. But now I'm wondering: maybe it is actually impossible to write such a proof checker, because there is no way for it to get around the halting problem and detect circular reasoning?