3 ms·

It’s a bit of a nihilistic view that programmers are merely slow boiler plate auto completion systems and our jobs will be replaced by AI. We already write mor

It’s a bit of a nihilistic view that programmers are merely slow boiler plate auto completion systems and our jobs will be replaced by AI. We already write more code than we understand given how lowly the industry regards formal methods and how divided it is even on testing. It is not surprising to me that Bertrand Meyer could miss that error in the code! A former colleague of mine challenged his grad students to implement an error-free version of binary search. He gave them the specification and verified each one: the majority of the submissions had errors. It’s a marvel that computers and software work so well. And instead of tackling the problem of programming, as Dijkstra put it, we’re going to automate writing more code. Great. See you in a few years when we can’t even keep up with the deluge of error prone programs. Although we have gotten this far with very few proofs and models. Who knows, maybe we’ll just tolerate it? It would be nice to have code synthesis work on larger examples from deep specifications. And models that understand proof tactics and can speed up the process of formalizing proofs. That would be nice.

sigstoat 4y ago
> A former colleague of mine challenged his grad students to implement an error-free version of binary search. He gave them the specification and verified each one: the majority of the submissions had errors. I was in a class on Isabelle where we had to write and prove correct a binary search function. As I recall, everyone admitted that their first function didn’t work.
- renewiltord 4y ago
  Java's was broken till '06
  - OnionBlender 4y ago
    https://en.wikipedia.org/wiki/Binary_search_algorithm#Implementation_issues https://en.wikipedia.org/wiki/Binary_search_algorithm#Implem... People often do (L+R)/2 but that can overflow. Using L+(R-L)/2 avoids the overflow problem.
    - nomel 4y ago
      As someone who has a binary search in their interview question, I will claim that far more people run into the problem of trying to do midpoint/2 and midpoint*2, long before overflows.
jasfi 4y ago
AI will be a major productivity enhancer. The things that make programming interesting will be what programmers focus on in the future. There's so much potential software that could be written that I don't think that the number of programmers will decrease at all.
- mbork_pl 4y ago
  This may be true, and it worries me. I have a (completely unproven) conjecture that things that make programming boring (like writing boilerplate code) are more or less things that let us avoid burnout. How many hours per day can you stay focused on difficult (or at least non-boring) problems? And for how many years? Whenever someone says "AI = productivity enhancer", I hear "AI = burnout accelerator".
  - jasfi 4y ago
    Burnout has different causes. For burnout because of intense work, it could be that the movement to reduce the number of hours we work will come at the right time. 4 day work weeks at 100%, for example. Lots of people experience burnout because writing boring code can be mind-numbing. Then there are people factors, such as a bad manager. Perhaps AI can give us more understanding management?
  - pydry 4y ago
    IME burnout is neither about boilerplate or traditional "interesting" problems, it's about "somebody else didn't do their job right" problems like the infamous "why can't I just serve 5 terabytes?" story or toxic work cultures. https://rachelbythebay.com/w/2021/10/30/5tb/ https://rachelbythebay.com/w/2021/10/30/5tb/ If it takes away the boilerplate and the interesting problems leaving us with just with 5 TB problems then yeah, burnout city.
- pydry 4y ago
  If programmer numbers decrease it won't be as a result of running out of things to code or AI, it'll be as a result of market consolidation within a few, extremely powerful firms who can squash most competitors like bugs. Like the US auto market - a once thriving ecosystem of fiercely competing innovative small businesses consolidated into 3 vertically integrated firms who now think innovation is building a slightly bigger truck. Of course, they'll probably blame it on AI coz a story about the inevitable march of technological progress invites less government oversight of the abuse of market power, and we will no doubt be plied with plausible sounding stories to that effect.
anonzzzies 4y ago
> See you in a few years when we can’t even keep up with the deluge of error prone programs. I think the worst case of this situation will pop up before that; not writing code at all but just hook the AI up, ‘prompt engineered’ directly like so; <body> <script>doInsuranceForm();</script> </body> Which will AI generate a html insurance form every time the page is requested and handle the user input etc. And it’ll be subtly wrong most of the time; it’s insurance, who knows if the current programmed forms are correct anyway (I know of at least one insurer that rounds off $0.01 wrong almost every policy because of using float for money on the web side). Why have the AI make code we can read? Just let it do the entire thing /s It’ll happen though and it will be used seriously by companies. The quality of the AI, legislation and public/consumer complaint fallout will determine if we get back to code that humans check. Being sceptical about humans wanting quality over paying as little as possible, I am going to say no.
foooobaba 4y ago
I think this idea of having formal methods integrated with AI code gen will be really powerful. If we can write verifiable specs, or even a way to automate approximate verification, then it can be used a s a scoring function to train an machine learning algorithm that performs codegen.

sigstoat 4y ago

> A former colleague of mine challenged his grad students to implement an error-free version of binary search. He gave them the specification and verified each one: the majority of the submissions had errors. I was in a class on Isabelle where we had to write and prove correct a binary search function. As I recall, everyone admitted that their first function didn’t work.

renewiltord 4y ago
Java's was broken till '06
- OnionBlender 4y ago
  https://en.wikipedia.org/wiki/Binary_search_algorithm#Implementation_issues https://en.wikipedia.org/wiki/Binary_search_algorithm#Implem... People often do (L+R)/2 but that can overflow. Using L+(R-L)/2 avoids the overflow problem.
  - nomel 4y ago
    As someone who has a binary search in their interview question, I will claim that far more people run into the problem of trying to do midpoint/2 and midpoint*2, long before overflows.

jasfi 4y ago

AI will be a major productivity enhancer. The things that make programming interesting will be what programmers focus on in the future. There's so much potential software that could be written that I don't think that the number of programmers will decrease at all.

mbork_pl 4y ago
This may be true, and it worries me. I have a (completely unproven) conjecture that things that make programming boring (like writing boilerplate code) are more or less things that let us avoid burnout. How many hours per day can you stay focused on difficult (or at least non-boring) problems? And for how many years? Whenever someone says "AI = productivity enhancer", I hear "AI = burnout accelerator".
- jasfi 4y ago
  Burnout has different causes. For burnout because of intense work, it could be that the movement to reduce the number of hours we work will come at the right time. 4 day work weeks at 100%, for example. Lots of people experience burnout because writing boring code can be mind-numbing. Then there are people factors, such as a bad manager. Perhaps AI can give us more understanding management?
- pydry 4y ago
  IME burnout is neither about boilerplate or traditional "interesting" problems, it's about "somebody else didn't do their job right" problems like the infamous "why can't I just serve 5 terabytes?" story or toxic work cultures. https://rachelbythebay.com/w/2021/10/30/5tb/ https://rachelbythebay.com/w/2021/10/30/5tb/ If it takes away the boilerplate and the interesting problems leaving us with just with 5 TB problems then yeah, burnout city.
pydry 4y ago
If programmer numbers decrease it won't be as a result of running out of things to code or AI, it'll be as a result of market consolidation within a few, extremely powerful firms who can squash most competitors like bugs. Like the US auto market - a once thriving ecosystem of fiercely competing innovative small businesses consolidated into 3 vertically integrated firms who now think innovation is building a slightly bigger truck. Of course, they'll probably blame it on AI coz a story about the inevitable march of technological progress invites less government oversight of the abuse of market power, and we will no doubt be plied with plausible sounding stories to that effect.

anonzzzies 4y ago

> See you in a few years when we can’t even keep up with the deluge of error prone programs. I think the worst case of this situation will pop up before that; not writing code at all but just hook the AI up, ‘prompt engineered’ directly like so; <body> <script>doInsuranceForm();</script> </body> Which will AI generate a html insurance form every time the page is requested and handle the user input etc. And it’ll be subtly wrong most of the time; it’s insurance, who knows if the current programmed forms are correct anyway (I know of at least one insurer that rounds off $0.01 wrong almost every policy because of using float for money on the web side). Why have the AI make code we can read? Just let it do the entire thing /s It’ll happen though and it will be used seriously by companies. The quality of the AI, legislation and public/consumer complaint fallout will determine if we get back to code that humans check. Being sceptical about humans wanting quality over paying as little as possible, I am going to say no.

foooobaba 4y ago

I think this idea of having formal methods integrated with AI code gen will be really powerful. If we can write verifiable specs, or even a way to automate approximate verification, then it can be used a s a scoring function to train an machine learning algorithm that performs codegen.