No, but I also think it's just not worth the effort for 99.99% of software. It's neat that it can be done when absolutely necessary, but that's not where most of the benefit of formal methods can be had. Also, you don't need many certified compilers, so the techniques used to construct them need not be scalable.
> SCADE is great, and it's "formal methods" in the sense that you write your program as a formal model with clear semantics that can be reasoned about. But it's not the kind of proof the OP asked about, I think.
Well, they wrote "I would image that certain languages are easier to prove (haskell vs C)", and SCADE is easier to formally reason about -- be it with a model checker, static analysis or deductive proofs -- than Haskell. Usually, languages with very simple semantics are easier to reason about either automatically, manually or semi-automatically, and the languages that are used in the industry in formal methods (except static analysis) -- even if the formal methods used aren't deductive because that's just too costly -- are those that really are "easiest to prove".
> proving what you need proving most -- the non-trivial stuff -- is never quick and easy
The OP asked for proving "many things" quickly. You can prove many things in Isabelle by writing something like "by induction n. sledgehammer" and waiting for the automated machinery to do the rest. This doesn't suffice for everything, of course. But it's good enough for "many things", including stuff that would take a lot more work in Coq.
> seL4 and CompCert -- while great achievements -- are neither good examples of formal methods
The OP said they are not aware of any "formal proofs for programs". These are some examples. Many of the other things you mention use formal models, but not necessarily formal end-to-end proofs.
> "end-to-end", namely global correctness properties are proven all the way down to machine code. This level of correctness is unnecessary for 99.99% of software; perhaps even for no software at all.
Compiler bugs are a thing. At Airbus, the generated assembly code is inspected manually for bugs introduced by the compiler (which is untrusted, and takes input C code generated by SCADE's untrusted code generator). You think that's useless voodoo?
> formal methods in industry include the use of SCADE
SCADE is great, and it's "formal methods" in the sense that you write your program as a formal model with clear semantics that can be reasoned about. But it's not the kind of proof the OP asked about, I think.