That's a load of crap. SPARK lets you practically throw together embedded programs with code-level proofs. CompCert was a huge leap over the non-optimizing, toy compilers that came before it. CRYPTOL specified algorithms at high level with C generation. LANGSEC is automating secure parsers. Another did protocols. The seL4 project included AutoCorres that can pull HOL specs right out of C projects. Verisoft gave us a full stack with processor (VAMP), C-like language, compiler, OS, and apps. Myreen and Davis have verified ASM, LISP, ML, extraction, provers, and hardware. Rockwell-Collins has a flow from Simulink models to specs and SPARK code for their mathematically-secure AAMP7G. Recent work verifies non-interference and other properties down to the gates.
There's been a ton of work knocking out whole categories of problems with no effort followed by other work that lets us do full verifications with a fraction of prior effort. You should read up on successes like those before claiming nothing has been going on. Heck, lets skip to one of the best where non-experts verify an ext2 filesystem in fraction of the labor it took to do seL4:
https://ts.data61.csiro.au/publications/nictaabstracts/8956....
Actually writing that code is still slow process.
Another example is the K framework where they just use rewrite rules in a decidable logic with some supported tooling. That specific theory, their logical strategy, let them do a whole semantics for C with undefined behavior included in just a few thousands lines of specs. In form of KCC, it can also be used as a compiler.
The oldest one, from co-inventor of software engineering, let you specify functional, structural, and resource requirements in a logical notation with the tool synthesizing about everything else for you. That was 001 Tool Suite. The thing is, I can only imagine tools getting much better than that because any development will require human brains turning problem descriptions, constraints, etc into precise statements. Which is what specs are. That we're already at spec-to-code synthesis and proof for some of these tools seems like something that can't be hand-waived away as "no theoretical breakthrough there just lots of new tools."
It would be some new idea in proof theory that would produce significant reduction of required manual work in practical applications, making it easier for humans to work out the proofs and proof assistants help humans.
Linear logic, affine logic, etc. can provide incremental advantages, not breakthroughs.
An example of one for exactly your types of programs is Microsoft's Xax:
https://www.microsoft.com/en-us/research/wp-content/uploads/...
My preferred approach is the old-school method of highly-assured microkernels that just separate everything else from one another. Here's a browser OS based on that principle:
https://www.usenix.org/legacy/event/osdi10/tech/full_papers/...
That kind of buys us nothing in terms of whether we'll know if programs are malicious or contain them, eh? And look at the giant, losing game that followed between the mice and the well-fed cats. It's why safety-critical systems often used deterministic, state-machines running on simple MCU's or PLC's. :)
Protocols like https, ssl and cryptography and operating systems would be my first choices.
So far only some military and safety critical applications and parts of Intel's silicon have been worth of the cost.
I took my first course in formal methods using the book Programming: The Derivation of Algorithms by A. Kaldewaij. It would be perfectly reasonable to implement something similar to Kaldewaij's guarded programming language today over some other programming language and use it to derive formally proven programs if someone really values the correctness. It would be also cool and fun but not for everyone.