Sigh. As I point out occasionally, the halting problem very rarely comes up in practice. Combinatorial explosion, yes, but not actual undecidability.

Understanding the implicit constraints of C/C++ functions is something where an LLM can help. Once you have the constraints recorded, they become formal constraints at the call. Historic C isn't expressive enough for even basic constraints.

Most of the constraints mentioned are at least expressible in Rust.