The Hundred-Year Language (2003)

Post by mvindahl » Tue, Mar 21, 2017, 9:48 AM UTC

TurboHaskal wrote: post #18

mvindahl wrote: post #15

"Beating the Averages" is also a good read. 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 b…

I also liked the article back in the day and drank the kool-aid. 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 t…

Dunno. I think for a startup it makes good sense to have a dynamic language with a good package manager. For someone writing something which needs to be performant, and the requirements don't change too much, C is probably a superior choice. It's all about tradeoffs IMHO.

Post by emtel » Tue, Mar 21, 2017, 4:30 PM UTC

daly wrote: post #2

There is a fundamental change in language coming. I believe that within 5 years the latest crop of programmers will begin to write PROVEN functional programs. Program proof technology has taken a giant leap in the last few years. These new techniques are starting to show up at Universities. Those graduates will know how to prove programs and, after the old programmers like myself die off, will simply expect that proo…

This won't happen to any large extent for the simple reason that in 95% of the software that people write, deciding what constitutes "correctness" (aka business requirements) is the bulk of the work. Further, those requirements change continually. Even if they could be frozen at a certain point, specifying them formally would be a massive undertaking, and the correct formal specification of those requirements would itself be a source of errors. How do you know when the formal specification means exactly what you really meant it to?

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.

Re: The Hundred-Year Language (2003)

Re: The Hundred-Year Language (2003)