>A far more feasible approach (though still very expensive) -- and probably a more "correct" one, even theoretically -- is to verify existing C code using some of the many excellent verification tools (from static analysis to white-box fuzzing and concolic testing) that exist for C
When I tried to verify C code (with hoare calculus, by hand) I found that rewriting that code in haskell and proving that to be correct was much easier. As a result i hardly know anything about the complexity of that code, but for me knowing it produces correct results was enough.
> When I tried to verify C code (with hoare calculus, by hand)
That's not the kind of verification I mean (proof of correctness, let alone deductive proof), but rather automated verification of "internal" program properties (aliasing, dangling pointers etc.), similar to those that could be achieved with type systems like those of Rust or Haskell. However, those tools could also prove stronger properties, probably with a bit more effort.
BTW, if you want to fully formally verify the correctness of C code, you don't need to do it by hand. There are tools that can help you (like Why[1] and various source-level model checkers).
When I tried to verify C code (with hoare calculus, by hand) I found that rewriting that code in haskell and proving that to be correct was much easier. As a result i hardly know anything about the complexity of that code, but for me knowing it produces correct results was enough.