Industry reality is that we are still fighting stack overflow bugs 40 years after safe languages were invented.
Timing attacks are going to be around a long time.
As devices become more powerful and more connected, thus increasing the attack surface and the potential losses form them being cracked, the cost-based analysis will start to prioritize security more.
The tools for writing dramatically less brittle code are there, but there's the cost of switching. It needs to become lower than the potential losses. And with the current state of the industry, the losses and lawsuits are surely coming. Remember what it took to make an average e-commerce website become reasonably secure.
Getting people to use heavy static analysis is an uphill battle. Getting people to use prepared statements to prevent SQL injection is an uphill battle! But nobody should take then lesson that we are woefully unprepared to deal with timing leaks via program analysis and that we've entered some new unfamiliar territory.
For example, here's Z in C++14, used to compute 5 factorial: https://godbolt.org/g/se5B8u
I think proving that no recursion exists should be relatively simple, just keep following the call graph and keep a set of the nodes (functions) called; you either reach the terminal node(s), or reach an already-visited node again, which means a recursion exists.
[0] https://en.wikipedia.org/wiki/Total_functional_programming
But sometimes it is hard, and I'm afraid it's equivalent to the halting problem in general case.
Without recursion, though, finding the maximal depth of the call graph is definitely solvable, and likely not even very hard.
Side note: an interesting case is the Stable Marriage Problem. It's easy to write the O(n) algorithm and prove its bound, but it's hard to translate into a bounded recursive algorithm that does the same thing.
(At least as far as I understand -- I searched it on Stack Overflow and that's what it said, and I've tried the problem itself. A Coq fanatic insisted that "if you can prove the run time is bounded it's easy to write the bounded recursive equivalent" but somehow that never translated into an actual insight on how to do it.)
There are still cases where you can prove that a recursion is bounded (I suppose something like dependent types could help here). There are definitely cases where you can prove that a loop is bounded, because the semantics of the language requires them to: a loop with a counter (not otherwise mutated), iteration over a known finite structure, etc.
Well, both C++ and Haskell allow you to use compiler features that are undecidable in general case, but usually work well in practical cases. Also, if e.g. your recursion / loop analysis is taking too long, you can just stop the analyzer. If the code can't be reasonably proved right, it should be considered wrong (with a chance of a false negative).