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.
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.
I read these essays for the first time a some years ago at a time when I was being assigned to a Javascript project and, much to my own surprise, had gone from ridiculing the language to secretly kind of liking it. At the time I had been working with Java for 10+ years and Javascript had always been regarded as this inbred cousin from Kansas that you didn't really want to be seen in company with.
Anyway, reading Graham's essays on computer languages helped me understand that Javascript was actually one rung up the abstractness ladder compared to Java, and that the language that I had always considered to be limited was instead extremely flexible and hence, stronger.
BTW, a curious thing about Graham is that he measures the strength of a language by how many features it shares with Lisp. Hence, no language will ever surpass Lisp using that yardstick.
Except that the averages ended up beating the nerds, which is empirically observed by glancing at today's most successful and widely used software; and Lisp today is a fringe idea with its most popular implementation being a JVM transvestite.
As for Javascript being an acceptable Scheme, I'm personally happy to see it merely running in the browser and the servers of a bunch of SV startups, where it cannot do harm to society.
Please don't do things to make titles stand out, like [...] adding a parenthetical remark saying how great an article is. It's implicit in submitting something that you think it's important.
Haskell. He's talking about something like Haskell - but with whatever additional powers of abstraction and simplification mankind manages to dream up.
I say this, because I have yet to find such an elegant way of expressing computation. But, on the other hand, I have yet to find a "serious" language with as many performance land-mines, which possibly might just not matter given orders of magnitude more memory and computing power.
Given a couple of orders of magnitude, who cares that String = [Char]. It's damned elegant.
For everything else, I'll bet we will use the "C" of the 21st century - Rust :-)
JavaScript will probably continue tracking functional languages like Haskell for many years, albeit remaining without the type system that make them truly useful.
Thank you for re-posting this long-forgotten essay, and taking me down memory lane...
(2003)
