The article isn't saying that letting errors happen is the best way to go about things in all cases. There is certainly room for proof and extreme caution! Tha

The article isn't saying that letting errors happen is the best way to go about things in all cases. There is certainly room for proof and extreme caution! That said, you do not need to prove everything about your algorithm. I imagine that in the future, we'll write software with base runtime system that has some basic sanity properties (proved) and on top of that, there will be layer that handles things in a more flexible way. Kind of like having Challenger JVM which is provably correct and never crashes and lots of apps on top of that :-)