Live data from Hacker News

The Hundred-Year Language (2003)

paulgraham.com

1–10 of 22 posts

Re: The Hundred-Year Language (2003)

#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 proofs are normal and required.

Re: The Hundred-Year Language (2003)

#4
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 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.

Re: The Hundred-Year Language (2003)

#5
post #4
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 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.

My own take on this is that we need to develop strongly declarative languages. That way there is no information about implementation to get wrong. You specify the "what" not the "how". You still might get the "what" of it wrong but this is no different than the mistake of "proving" the wrong thing. Eventually there will be strong AI and we will be able to pass off the "what" of it to the machines as well.

Re: The Hundred-Year Language (2003)

#6
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…

Can you point out which specific advancements in the last few years you are talking about?

Re: The Hundred-Year Language (2003)

#7
Please don't use article titles to editorialize. From https://news.ycombinator.com/newsguidelines.html:

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.

Re: The Hundred-Year Language (2003)

#8
post #4
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 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 more work

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.

Re: The Hundred-Year Language (2003)

#9
post #6
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…

Can you point out which specific advancements in the last few years you are talking about?

It's not so much fundamental advances as much as a maturing of tooling and educational resources. The result is a lot of compelling proof-of-concept implementations:

https://sel4.systems/

http://compcert.inria.fr/

https://cakeml.org/

Re: The Hundred-Year Language (2003)

#10
post #7

Please don't use article titles to editorialize. From https://news.ycombinator.com/newsguidelines.html : 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.

Sorry about that. I would definitely change the title if I could but it seems to be permanent now. Thank you for the feedback.
Post reply on HN