> tracking how many times a function can possibly recurse.
> Tracking recursion is definitely possible, as shown by proof languages like Agda or Coq that make you prove termination of recursive functions
Proof languages don't really track how many times a function can possibly recurse, they only care that it will eventually terminate. The amount of recursive steps can even easily depend on the inputs, making it unknown at the moment a function is defined.
Right. They use rules like "a function body must destructure its input and cannot use a constructor" which implies that, since input can't be infinite, the function will terminate. That doesn't mean that the recursion depth is known before running.
The actual rule is more refined than that and doesn't prevent you from using constructors in the body or recursing without deconstructing any input, it just needs to prove the new inputs are "smaller" according to a fixed well-ordered relation. This is most often related to the structure of the input but is not required. For example I can have f(5) recurse into f(6) if that's "smaller" according to my custom relation, but no relation will allow me to continue increasing the argument forever.