But the theory is written into real programs by humans, who make mistakes. The math is unassailable until, oops, it isn't, because someone forgot a bounds check!
This whole "move fast and break things" philosophy should be unacceptable, if you want people to trust in your new cryptocurrency/voting machine/etc, but try telling your investors that it'll take 5 years to develop the software instead of 5 weeks to "a first prototype" whose bugs and bad design decisions will haunt you forever...
2) Extraction is not the only approach to verifying software with Coq (see Verifiable C, or Bedrock). In other proof assistants, e.g., in Isabelle or HOL extraction isn't even available and so other approaches are common. For a nice example look at the bootstrapping process of CakeML (https://cakeml.org/).
3) Even if it wasn't, the point is that the trusted base with verified software is tiny compared to anything else that people are actually using. "It's not perfect" is not an excuse if it is basically perfect in practice. See the Csmith paper ("Finding and Understanding Bugs in C Compilers", https://embed.cs.utah.edu/csmith/) and what they had to say about CompCert.