The Holy Grail of Static Verification and Static Typing

There is no such thing.

It’s a trade-off. Even in computers, there is no such thing as perfectly reliable code, there’s only how much resources you’re willing to pay for the next improvements. It’s easy to be oblivious to this. I can’t even count the number of times said some variation of “OK, now I know it works” before I learned that it will always break. Always.

Failure is inevitable. If you want to build anything large and to last, you have to incorporate it into your design and build organic systems that monitor, recover, repair, and, above all, fail gracefully when they themselves inevitably fail.

Holy Grail этот самый, короче, достижим только в случае неизменного окружения, неизменного ТЗ и исключения человеческого фактора. Чего в природе не бывает.