Coq and similar languages are definitely quite expressive, but they're still complex enough to involve non-trivial manual intervention. Verifying something with Coq is possible but it's hard; whole PhD theses have been written around verifying code for a single program. I know there is some proof-search-based automation available (ie auto), but I understand it's still pretty limited.
Coq, Agda and similar languages are restricted enough to make verification possible, but complex—and expressive—enough to make it very difficult to automate.
The opposite extent would be domain-specific languages that are very restrictive but still powerful enough for their domain. Designing languages like that would let us verify non-trivial properties fully automatically and can save a lot of work for the user, but we end up needing to design a language for each class of task that we care about.
As I said: it's an interesting design problem.
One recent addition to this is the Lean theorem prover, which tries to be similarly powerful and general as Coq but with more provisions for automation via the Z3 SMT solver. I haven't played with it myself but from what I've heard it's a very promising development in making formal verification more accessible to non-experts.
> Coq, Agda and similar languages are restricted enough to make verification possible, but complex—and expressive—enough to make it very difficult to automate.
Pretty much every theorem proving system out there is expressive enough to state whatever program property you want. You can't escape having to automate proofs though.
> Coq and similar languages are definitely quite expressive, but they're still complex enough to involve non-trivial manual intervention. Verifying something with Coq is possible but it's hard; whole PhD theses have been written around verifying code for a single program.
Yes, it's the most challenging aspect of programming I've ever tried. It's completely impractical and too expensive for most projects right now outside of domains where mistakes cost even more like aviation, medical devices, operating systems, CPU etc.
> The opposite extent would be domain-specific languages that are very restrictive but still powerful enough for their domain.
I'm not really sure what the sweet spot is to be honest or if there is one when you require full automation. Even non-linear arithmetic is undecidable (basically arithmetic where you're allowed to multiply variables together) so you quickly get into undecidable territories for what seem like basic properties. No clever language design idea is going to let you side-step that proof automation is hard which has been worked on for decades. Even writing program specifications requires a skillset most programmers will have to learn.
Coq, Agda and similar languages are restricted enough to make verification possible, but complex—and expressive—enough to make it very difficult to automate.
The opposite extent would be domain-specific languages that are very restrictive but still powerful enough for their domain. Designing languages like that would let us verify non-trivial properties fully automatically and can save a lot of work for the user, but we end up needing to design a language for each class of task that we care about.
As I said: it's an interesting design problem.
One recent addition to this is the Lean theorem prover, which tries to be similarly powerful and general as Coq but with more provisions for automation via the Z3 SMT solver. I haven't played with it myself but from what I've heard it's a very promising development in making formal verification more accessible to non-experts.