> You don't have to let the ATP do everything, you can speed it up immensely with well placed assertions where it struggles.

This is basically what you do with Dafny. I'm not very happy with this, not least of which is because it makes for an inferior developer experience in my opinion and because in general you are pretty limited in expressiveness of propositions.

Also it's kind of weird to be fixated on ATPs, as those are more or less a different level of abstraction from the language. You could develop an ATP for Bend.

More generally speaking, the largest, most well-known formal verification projects that verify actual code don't really rely on ATPs. SeL4 relies on explicit proof terms, CompCert relies on explicit proof terms, etc.