In some circumstances, static proofs are also possible. IIRC it's still an open problem in zig as to what the possible language features will be while keeping this guarantee, but the goal is to be able to have recursion in some circumstances and still provide the possibility of stack-overflow-safety with a performance tradeoff, and to know when you've stepped out of the bounds where that is possible.
Here's a thread I'm at least a year out of date on https://github.com/ziglang/zig/issues/1006
The general philosophy is to give the programmer tools to know what the consequence of a choice will be as far as that doesn't hamstring them overly. Ie. the compiler can tell you when a stack overflow is possible, and it's up to you to decide what to do about it (or whether it is wrong because you know something it doesn't).