I read this and thought, "oh, the author is calling out formal verification as overhyped? Hillel Wayne (https://hillelwayne.com/) is going to be angry! Wait, who wrote this..."
Overhyped is not the same thing as bad. I program in common lisp, it is by far my favorite environment for developing. I also think just about every blog post and reddit comment by someone who has just discovered lisp greatly overstates its advantages.
I recall that F Scott Fitzgerald said "the test of a first-rate intelligence is the ability to hold two opposed ideas in mind at the same time and still retain the ability to function."
In Hillel's defense, maybe they're not opposed ideas... this article talks about problems with formal verification, but I think his thing is more formal modeling (with TLA+).
