An example of something you can formally verify with proofs in Software Development
Look into tools like Frama-C, SPARK, Astrée, etc...
They have their use in very specific cases, notably software verification of small to medium sized embedded safety critical software (e.g. inside aircrafts, per DO-178C, or nuclear power plants, etc...). Such software have a few dozen thousands lines (or perhaps two hundred thousands at most of C or Ada code), but a bug inside them could crash a plane. So the industry is ready (and required by external regulations) to spend a lot of money and efforts on such small critical software. There are also many severe coding rules (e.g. dynamic allocation, recursive functions, dead code are forbidden).
Proving software, even with these tools, is very costly. A typical safety-critical software costs about a hundred or a thousand times more to develop than a usual software (like your phone applet or some Unix command line tool) of equivalent size, because formal methods (but not only them) are involved. The teams developing them should have formal methods experts working together with aircraft software experts. Sometimes, a small routine has to be rewritten and annotated to be processable by code provers.
There are several research projects around such tools and their use. For a recent example look into VESSEDIA (but you could find many others). One of its results might include a simple proof of a small subpart of the Contiki OS. From an outside view, the results are related to simple subsystems of it (e.g. some simply-linked-list module). In practice the proof requires a lot of formal annotations (so the developer has to provide annotations in ACSL about half as long as the simple C code that is specified by these annotations).
The L4 microkernel has also a variant, called seL4, which uses formal methods (the code size which is formally proved is a few dozen thousands of C code). AFAIU that variant (with its proof) is open-source.
But formal methods don't scale well. It is very unlikely that they would scale -in the next 20 or 30 years- (for present-day programming languages and code) to software as big as the Qt toolkit or the Linux kernel (because formally specifying the intended behavior of Qt or of Linux kernel is practically impossible). For example, C heap allocation is easy to code (that is, a lot of C code uses malloc &amp; free), but difficult to formalize and prove (because current shape analysis techniques don't scale well to large programs). That internal complexity and difficult of formal methods hinders its uses in real-world programs (whose size is growing a lot: a source code editor today is much more complex and bigger than what vi was in the 1980s).
I was part of several research grant submissions mixing more or less formal methods and other approaches (e.g. machine learning techniques on large amount of code, natural language processing techniques), but such funding is hard to get (e.g. there is probably no more any H2020 or FP9 calls dedicated to software engineering before my retirement; the last one was ICT-16 to which I was part of a submission -and waiting (in june 2018) for its evaluation; but only a few percents of submitted proposals get funding). See also this answer to another (but indirectly related) question. BTW, I might be interested in joining some European consortia in 2019 for HPC software tooling using such ideas.
To summarize: There is No silver bullet, so I agree with you:

there is no use in Hoare Logic or Operational Semantics in practical software development

(because even if you have proven your code w.r.t. some explicit formal specifications, there could be - and there still is some - &quot;bugs&quot; or incompleteness in the formal specifications; specifying &quot;correctly&quot; what a real-life software such as a word processor or some web application should do is practically impossible, since you want that specification to be &quot;complete&quot; and cover all the practical cases).
However, notice that recent practical programming languages (e.g. Rust, Ocaml, and also monsters like C++20 or C++17 which became so complex that only a dozen of people understands them fully) have been inspired by formal proof techniques. And academic curiosities like Agda uses even more them. Also, static source code analyzers like clang-analyzer (and even some optimization passes of GCC) use techniques related to formal proofs.
Regarding CompCert, you could download its source code (and proof) and study its code, but you are not allowed to use that source code for non-academic purposes (so CompCert is not free software but its source code is downloadable and you are allowed to study and experiment it. However the resulting binary has license restrictions).
See also this draft report (and the references there).