It depends on what kind of guarantees you want, and how much you rely on the language versus programming style. But I think there are fundamental reasons that w

It depends on what kind of guarantees you want, and how much you rely on the language versus programming style. But I think there are fundamental reasons that would prevent you from doing development in full Common Lisp and expect a formal verifier to statically check your code for complex properties (such as halting, bounded memory), and expect it to never reject a correct program. Even with functional languages, the stronger properties you want to check, the more restricted the program must be. For example, Idris can ensure your program halts, but it requires you to write your program in a specific way that can be checked for halting, you can't just take any halting program and expect it to pass the halting checks. Similarly, Rust's borrow checker can verify if your program is free of data races and memory leaks, but you must write your program following specific patterns, even if you can produce data-race and memory leak-free programs in other ways as well (of course, there is the `unsafe` block in Rust exactly for this reason). Of course, there will likely be more improvements as time goes on, but the halting problem puts a fundamental limit on how expressive a language can be while also being amenable to (computable) proof of certain complex properties.