I am fine with statically checking types, or any kind of proof. Are your floating points calculations always precise enough? Can you detect if no user inputs ever reaches critically secure code without being sanitized? Does this multi-threaded code ever deadlock? There are plenty of things that can be made to guarantee properties you care about, and the reason you do not always use them is because of budget (time, money). Do you always write contracts around your stuff? is it a good contract, not one that just repeat what your code does? If you don't, please understand that I don't always use static types for everything and in all cases. Also, my code is not purely functional either.
If I need to do smart things in Lisp ahead-of-time, I may want to use a DSL and prove whatever I want to prove on it, and generate correct-by-construction code that does not check things at runtime. I could use ACL2, too. Please note also that I can work in a different language when it makes sense.
3) Statically typed compilers include Lisp ones. My code is sometimes underlined in orange like yours, because I made some dumb typo or because types do not match. Likewise, optimizations are done too, in particular inside functions, where things are more static than in the global environment.
What about efficiency? Look at the postal system: you have to wrap letters and objects in enveloppe or packages (except postcards, which are like fixnum), put a label on it with many informations... what a waste of time and space!
Yet, each object has a type now and can be dispatched reliably and efficiently. If you put your letter in the wrong box, you will have enough information to recover and perform your job. Once letters are all filtered out from packages, you can avoid checking that they are letters and gain some efficiency. You can build a new kind of service (drone-delivery?) with a special label and dedicated rules and integrate it within a running system without restarting the world. If anything goes wrong, you can have a generic error handling mechanism that does not crash everything. Static types are more like pipes: clean water here, used water there, and they never mix in a wrong way thanks to pipe calculus. So while I agree that static analysis can be great for doing crazy optimizations, there are use-cases where dynamic typing shines, and generally people replicate that using tagged objects anyway: think about game entities which are "typed" dynamically, or frameworks when you can load custom scripts (and those are generally not typed-checked, unlike Lisp).
2) You plan for failure. Even in a statically-type language, you'll have runtime bugs. Only in a mission-critical system are errors fatal. If you place restarts or error handlers accordingly, you'll have the opportunity to fix your stuff. Ask Erlang people about reliable systems.
1) Worse, you compile your code, the compiler complains but you can still run the produced code! Then you can test your error-handling code.
Seriously, this is not a problem in practice. Coding and testing are interleaved because the environment is right here awaiting orders. If you look at the end-result, I am doing the job of the static type checker by fuzzying input in a way that makes sense for that particular function. I also have a global view of the system and more context to decide what will happen at runtime, or not. When I fail (I am not proud of it, like most static analyzers), the runtime is here to catch it.