Not a stupid question at all. There are two reasons verification tends to happen in these specialized languages: the languages we usually use are often not expressive enough to write things like specifications, and a bit too expressive in the sense of letting people write program logic that is insanely difficult to verify (think untyped pointers into a dynamically allocated heap for example). So these verification related languages often are more expressive on the spec side and more restrictive in terms of what kind of code you can write.

> … verify/synthesize invariants in languages people use?

Good question. This is the holy grail. This is what everyone in PL research would love. This is where we want to get to.

Turns out a language as “simple” as C has sufficiently complicated semantics as to limit rigorous analysis to the basics. One example is loop analysis: it’s very useful to know that a loop will terminate eventually; if a loop is modifying some state and—worse—if the iteration variable gets modified—kiss your analysis goodbye because mechanically synthesizing strong pre- and post-conditions becomes insurmountable. It’s not an engineering challenge. It’s a math/pure CS theory challenge.

Most existing mainstream languages aren’t expressive enough to encode these invariants. For languages outside of the mainstream, Lean 4 is a language supporting verification, and it’s also a full programming language, so you can write your proofs/theorems in the same language that you program in.

That's what we use when we can limit our loop count and recursion depth somehow. Prove it for small data, and infer from it for big data.

I use C and C++ model checkers, like cbmc and its variants (esbmc) successfully, but you need to adjust your tests and loops a bit. Like #ifdef __VERIFIER__ or #ifdef __CPROVER__ https://diffblue.github.io/cbmc/cprover-manual/index.html

The semantics of Dafny is carefully designed to make verification efficient.

Dafny can compile to and interface with a few languages, including C#.

Dafny has been around for a while and people do in fact use it. People also apply contract languages to C and all matter of other things, so really question boils down to "Why arent you doing what I expect of you?"