Programmers may hate writing test cases and generators and proofs, but one thing they all seem to love is some good optimization. Flip a compilation flag and your program is smaller and faster!
And I think that is the key to solving this whole dilemma. Optimization and Verification, in terms of what they require from a program, are best buds. Quite a while ago, John Regehr wrote a blog post on the future of compiler optimization, where he suggested that verification and optimization will join forces, as well as some reasons and examples for why that should be [0].
Get people into languages and frameworks that are pushing the boundaries of optimization, and you'll find not only infrastructure that is ripe for correctness research, but large codebases solving real world problems. For example, Rust's MIR is a fully typed intermediate language that bridges the gap between LLVM-IR and Rust. It was created to help solve some ergonomic issues that made writing rust programs difficult, as well as for future optimization potential. And its existence should be a goldmine for correctness researchers. You have large open source codebases like Servo, written in a strongly typed language with a richly-typed intermediate assembly-like language that is just waiting for verification systems to be built on top of.
Optimization and verification have already joined forces: just look at CrellVM [0], which made the rounds on HN some weeks ago.
Also, as you mentioned, better type systems could be another nice byproduct.
Why wouldn't that be an opportunity for optimization? At the very least, feature X that only works with feature Y is dead code when feature Y is not present. Even if you only enable feature X when the user chooses to enable feature Y, you have some opportunities for whole program optimization across the code boundaries of X and Y.
And I think that is the key to solving this whole dilemma. Optimization and Verification, in terms of what they require from a program, are best buds. Quite a while ago, John Regehr wrote a blog post on the future of compiler optimization, where he suggested that verification and optimization will join forces, as well as some reasons and examples for why that should be [0].
Get people into languages and frameworks that are pushing the boundaries of optimization, and you'll find not only infrastructure that is ripe for correctness research, but large codebases solving real world problems. For example, Rust's MIR is a fully typed intermediate language that bridges the gap between LLVM-IR and Rust. It was created to help solve some ergonomic issues that made writing rust programs difficult, as well as for future optimization potential. And its existence should be a goldmine for correctness researchers. You have large open source codebases like Servo, written in a strongly typed language with a richly-typed intermediate assembly-like language that is just waiting for verification systems to be built on top of.
[0] https://blog.regehr.org/archives/247