I don't quite understand what big point this is trying to make. It's very down on formal verification, but does that mean all formal verification should be thro

I don't quite understand what big point this is trying to make. It's very down on formal verification, but does that mean all formal verification should be thrown away? Strong static typing? It's generally possible to write valid programs (i.e., that would run successfully without runtime errors) that don't type-check successfully. So the set of type-safe programs is smaller than the set of useful programs. Is that an argument for discarding type safety? No, because the vast majority of programs we want to write can be type-checked and it's useful to do so. Termination checking? This post has a nice example of an effectively-non-terminating loop in Bazel. Bazel's control language doesn't have unbounded loops, so the author just nests a bunch of very long loops. It's fun, but "it's possible to write a Bazel build script that takes an infeasibly long time to run, effectively infinite" doesn't seem like a problem in practice. It's still hard to write such a thing accidentally!