I've wanted to write a backend web programming language that is based on non-terminating/bounded principles. My theory is that all functions can prove to the co

I've wanted to write a backend web programming language that is based on non-terminating/bounded principles. My theory is that all functions can prove to the compiler that they have bounded execution based on the state and arguments given, and that X is the lower bound and Y is the upper bound. This propagates all the way to the entry point. I agree with the author with regards to the stronger semantics, and that's why I thought of this language. You often want to have some guarantees over the execution time of your program. It would probably be PRF based at the core, but Turing complete in practice. Like how rust rejects invalid borrows but still offers unsafe for raw pointers, this lang would either calculate the upper bound based on the simple loop primitives, or you'd have to use the unsafe operators and provide an alternative formula for the bounds.