It's a nice read, an important topic, that of not trusting blindly formal proofs. No theorem ever applies to real world objects, it can only say facts about ideas. It's good to keep that in mind but at the same time that's all we got, it's like a basic premise of science. That's why it's important be able to also do testing and have executable models, to validate that the model behaves like you think it should. But it's also what serious people do already even when doing formal proofs. And it's also why there's usually a difference between scientifically "solving" something and the art of making it actually work.