I meant to write every global property due to Rice’s theorem.

And I don’t believe my claim is unsupported, the largest formally verified program is the mentioned sel4, which is still tiny compared to even the smallest of business apps and was written by domain experts over multiple years.

Restricting a problem to a subset is like the numero uno step to solve any hard problem - and this is what rust basically mandate. It won’t provide bug-free programs, but it can reliably prove the absence of memory bugs and data races due to the borrow checker, which can do its work on function-scope, since all the relevant information is encoded in the function’s generic lifetime arguments.