"It baffles me that people think they can solve the problem of the intractability of systems by piling up more complexity on top."

The systems that ran for over a decade without downtime weren't done by formal proof: they had lots of review, checks and redundancies that came from prior experience with failures. Tandem NonStop comes to mind with VMS clusters getting pretty far. Identify a problem, develop a mitigation that works for all inputs, review it, test it, and deploy. Integrate with careful review and thorough testing. Whereas, a number of systems that were "proven" have failed after basic review or testing. Proof is just one tool among many instead of anything to think of as necessary or perfect.

Far as empirical evidence, those prior systems plus current ones with the most uptime or correct functioning in industry didn't have formal proof or use languages you'd recommend. That shows they're not necessary to achieve that goal. Formal proof with realistic models indeed showed the highest level of correctness once the tools matured. The drawbacks were: cost was insanely high, the models required overly-simplistic implementations, and time-to-market put them behind competition which can kill a company in markets. So, I recommend most don't do that kind of stuff. Whereas, I recommend CompSci do a mix of developing productivity/maintenance boosters (eg Racket, refactoring aids), optimizations, push-button tooling for verifying apps in popular languages (eg Pathfiner, Astree Analyzer) and clean-slate, verified stuff like miTLS or CompCert that can see real-world use without requiring specialists. Gotta balance across what people care about.

"The excessively operational definition of pretty much every Lisp dialect in existence makes it prohibitively expensive to formally analyze the humongous swathes of code generated by Lisp macros. "

The simplicity of it should make a SPARK-style analysis easy if the meta eventually decomposes into simple functions or operations with contracts describing intended structure or value ranges. The macros themselves can also be proven to be certified generators. Anyway, I think it's easier to address your point by comparing the base language to LISP in terms of ability to write a formal semantics or easily analyze it. Most mainstream languages fail immediately. A subset of LISP is doable given ACL2, VLISP and Myreens work. SML seems to win overall since it was designed for this but looses on many practical fronts like performance, developer tooling, and library ecosystem. Ocaml subset is closest to the goal for ML's but still behind mainstream stuff on factors more important to developers. Maybe Haskell, too, given verification tooling for it I've seen but I don't know its semantics so can't say more.

In any case, you'd be trading everything that gives developers velocity on software development for the ability to formally prove something more easily in the language which 99.999% of developers won't do. They can reach higher than their QA goals without it using lightweight methods with empirical proof of effectiveness above. Also, 99+% of proof engineers won't care about provability of base language either since they prefer to use dedicated tools with an extraction (eg CompCert) or equivalence check (i.e. seL4). If real-world deployment, people wanting a proven component can also prove it down to ML, C or ASM to wrap with a FFI (eg miTLS pieces in Firefox) or hide it behind an API (eg MULTOS CA in SPARK/Ada/C++ mix). Things like linking types by Patterson and Ahmed will make that safer over time.

"This sounds insanely complicated. The only justification I can come up with for this kind of thing is manager thinking: “This process has lots of steps and makes people's lives miseable, hence I must be doing something right!”"

I already gave you the reason: get confidence or defect rate close enough in practice to formal proof that software will meet its specification or fail safe taking developer right to error... without costs or time-to-market impact of formal verification. At most, we might be talking one well-trained, median programmer added per team instead of a proof engineer. Managers barely care about software quality on average much less formal proof. Selling them on improving defect rates at low cost in ways that makes extensions or maintenance easier is much more likely to succeed. Good example below by a Lockheed person on Design-by-Contract comparing it to other methods:

https://www.win.tue.nl/~wstomv/edu/2ip30/references/design-b...