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+...
As an example, I heard a story about an ambulance dispatch system that was built using formal verification. One of the things the developers wanted to prove about the system was that after an emergency call, an ambulance would always be dispatched within a certain amount of time. This seemed like an easy requirement to formalize: "For any dispatched ambulance A, the time of dispatch minus the time of call must be less than T".
Unfortunately, after the system was deployed, it turned out that occasionally an ambulance would simply never show up in response to a call. This seemed impossible until the developers realized that the proof still held, it was simply vacuously true in this case.
The fix is obvious in hindsight: The requirement should start with "For any emergency call...". But the point is that it is possible to make mistakes in requirements, just as it is possible to make mistakes in implementation.
Formal proof is no silver bullet for software.
I've recently tried out Elm [1] and have come away with a similar perspective on functional programming and static typing. The benefits I noticed are:
- Because of the static typing and strict management of data/state, the compiler is very good at telling you where the errors in your code are.
- If the compiler is happy, there are essentially no runtime errors.
- While I didn't write any tests, unit testing seems like it would be trivial because every function is stateless.
- You're forced to write better code. I find that Elm is pleasantly constraining. It's an opinionated language that forces you into certain design patterns, but they always seemed like the design pattern I should be using anyway.
Overall, I haven't been more impressed by a language since I discovered Ruby a decade ago. If you could do backend development in Elm I would probably try using it as my primary language.
1. If anyone else is interested, I went through the Pragmatic Studio Elm course: https://pragmaticstudio.com/courses/elm. I have no affiliation with them, just thought it was a really well done course and would recommend it to others who want to try out Elm.
I don't see any case for a functional-programming inspired change now. 30 years ago programmers were enlighten by LISP, 15 years ago I was enlightened by OCaml, and today's generation is enlightened by Haskell, or in your case Elm. What's different now?
If anything I think we're moving in the opposite direction. Development speed is now king, and deployment is easier than it's ever been, which means that bugs are less costly to fix. Bondage-and-discipline type languages that promise fewer bugs for more work are just less relevant.