> There's a lot of research that needs to be done before proven programs can become the norm.

At least equally importantly, we need a new generation of developers to grow up with these tools before they can become the norm.

In fact, the biggest contribution that academia could make to safe programs is to replace Java and C by Rust in all the programming courses, so that the next generation of developers is raised on Rust and makes that language (and its strictness mindset) popular in the industry in the same way that Java's relevance in the industry is based (in part) on its prevalence in curriculums.

As Zalastax was saying, by the standards of Coq, Rust doesn't have a strict mindset.

Rust isn't the first language to emphasise correctness. We've had Ada for decades, but it's not taken over the world.

Going to the extreme, full-bore formal methods will never be taught as introductory material on programming courses for the masses, but they will continue to be taught at good universities.

I'm not sure this is a bad thing. For most applications, ad-hoc develop-and-test makes good sense. RAD is important in some domains. Both formal methods and highly strict languages have their downsides.

There's more to correctness than language, of course. A shift toward correctness could be as simple as encouraging students to put runtime asserts in their Java code.

I hope we'll see more advanced type features added to languages. I find it very annoying when I can't be expressive enough and have to resort to comments and runtime errors. It's a very fine line to walk though. TypeScript is the language that I think is best at walking that line currently.