Speaking as a MIRI employee, I can say that MIRI isn't trying to build AI that's mathematically provable to be safe. This misconception comes from the same place the "AI safety engineering, etc." post is speaking to -- the assumption that if (e.g.) we do work in provability theory to develop simple general models of reflective reasoning, then the finished product must fall within provability theory.

Smarter-than-human AI systems will presumably reason probabilistically, and all real-world safety guarantees are probabilistic. But theorem-proving can be useful in some contexts for making us quantitatively more confident in systems' behavior (see https://intelligence.org/2013/10/03/proofs/), and toy models of theorem-proving agents can also be useful just for helping shore up our understanding of the problem space and of the formal tools that are likely to be relevant down the line -- the analog of "calculus" in the rocket example.

Yes. I've noticed this too on other threads talking about AI safety. The recent advancements in machine learning that are creating all the hype and industry interest have all been through the complete opposite approach that MIRI/AI safety researchers is taking. These advancements have been largely driven through empirical research, incremental engineering, trial-and-error practice, and rules-of-thumb (I am basically describing the state of deep learning research).