This contradicts the evolution of languages, they don't evolve into making people do more work. It's way more likely that writing proofs will never become a thing, but academia will simply get too out of touch to be even noticed.
They don't evolve into making people do less work, either! You really think programmers work fewer hours today than they did 40 years ago? They don't. They just build much more complex systems.
Languages evolve to meet people's needs. The question is, does the world need less buggy code code? I think the answer is yes.
Furthermore, you've made a huge assumption -- that proofs = more work. I expect that, eventually, our industry will become mature enough that the cost of bugs, vulnerabilities, etc. is properly priced and the current "move fast and break things" approach will fall by the wayside.
You can already see these methods being applied at scale in industries where "beat the other guy by a month" isn't important, but "don't crash the thing and kill 100 people" is.
This sounds to me like implying there are no recalls of goods by manufacturers in "matured" industries. But we have tons of recalls for cars, toys, food and gadgets. And that's just the tip of the iceberg, most bugs and vulnerabilities are never fixed. Even banking (remember the banking crisis?), insurance, infrastructure projects (airport BER) or utilities like power generation show that they don't work like you suggest matured industries work by at scale.
So what are the industries you're talking about that work at scale by "don't cash the thing"?
Most of these recalls aren't related to software. Regardless, systematic quality issues in each of those businesses have their own unique cultural origins.
> So what are the industries you're talking about that work at scale by "don't cash the thing"?
Aerospace, for one. Also chip design and fabrication.
And the old guard is even worse - recall Jeep's entertainment unit remote hack, or Toyota's 10,000 global variables? Those guys can't handle basic software engineering practices, let alone formally verified programs.
Aerospace and chip design are the two major industries that make regular use of formal methods.
> Uber and... Tesla... cowboying... And the old guard is even worse - recall Jeep...
Yes, most of the auto industry has been slow to the table when it comes to taking software quality and capability seriously.
Uber has a prototype, not a product, and Tesla has a young product. We'll see what engineering practices they adopt over the next 15 years.
> The idea of formally verifying a DNN image classifier seems absurd
https://www.google.com/search?q=verification+of+deep+neural+...