5 ms·

> Is this really the future of programming? Not the one I want. I'd like to see better theorem proving, proof repair, refinement and specification synthesis.

> Is this really the future of programming? Not the one I want. I'd like to see better theorem proving, proof repair, refinement and specification synthesis. It's not generating code that seems to be the difficulty, it's generating the correct code. We need to be able to write better specifications and have our implementations verified to be correct with respect to them. The future I want is one where the specification/proof/code are shipped together.

YeGoblynQueenne 4y ago
>> I'd like to see better theorem proving, proof repair, refinement and specification synthesis. Thanks for making me smile. Some of us are working on exactly that kind of thing :)
qsort 4y ago
Can't +1 enough. This is clearly the future, as the increasing popularity of type systems shows. As interesting as those systems may be, they have it exactly backwards. Don't let the computer generate code and have the human check it for correctness: let the human write code and have the computer check it for correctness.
- zozbot234 4y ago
  > let the human write code and have the computer check it for correctness. Isn't that pretty much what ML does?
  - goatlover 4y ago
    How would ML know what the correct code should be?
  - kristjansson 4y ago
    That’s exactly the inverse of copilot and LLM code generation. The computer generates the code, the human checks if it’s correct
    - rmbyrro 4y ago
      I bet most humans won't check. See the mindset of the author: > ... I will not delve into the questions of code quality, security, legal & privacy issues, pricing, and others of similar character. ... Let’s just assume all this is sorted out and see what happens next.
- john_the_writer 4y ago
  Actually both don't work. The human also needs to make sure the code does what the Ticket asked for. And sometimes not even what the Ticket asked for, but what the business and user want/need. Honestly writing code is such a small part of a dev's job. It's figuring out how to translate the human (often non-tech) requirements into code that is also in a way that's also looking at requests that haven't been made yet.
monkeydust 4y ago
Machine readable specs? Something along lines of this perhaps... https://www.fixtrading.org/standards/fix-orchestra/ https://www.fixtrading.org/standards/fix-orchestra/
- kimixa 4y ago
  Aren't "Machine Readable Specs" a programming language?
galdosdi 4y ago
> It's not generating code that seems to be the difficulty, it's generating the correct code. Also, it's not actually writing the code that is the difficulty when generating code changes for maintaining existing code, but figuring out what changes need to be made to add up to the desired feature, and where in the codebase controls each of those, and possibly rediscovering important related invariants. For that matter, the really critical part of implementing a feature isn't implementing the feature -- it's deciding exactly what feature if any needs to be built! Even if many organizations try to split that among people who do and don't have the title of programmer (eg business analyst, product manager...), it's fundamentally programming and once you have a complex enough plan, even pushing around and working on the written English feature requirements resembles programming with some of the same tradeoffs. And we all know the nature of the job is that even the lowliest line programmer in the strictest agile process will still end up having to do some decision making about small details that end up impacting the user. Copilot is soooooo far away from even attempting to help with any of this, and the part it's starting with is not likely to resemble any of the other problems or contribute in any way to solving them. It's just the only part that might be at all tractable at the moment.
marcosdumay 4y ago
The unsettling part is that something like Copilot requires a lot of the work that would need to create an amazing semantic-aware linter like no other on the market. Instead, they decided to waste their work on that.
- zokier 4y ago
  > amazing semantic-aware linter like no other on the market. AWS has ML driven code analysis tools in their "CodeGuru" suite: https://aws.amazon.com/codeguru/ https://aws.amazon.com/codeguru/
rvdginste 4y ago
Exactly! A couple of years ago, we invested in using the libraries from Microsoft Code Contracts for a couple of projects. It was a really promising and interesting project. With the libraries you could follow the design-by-contract paradigm in your C# code. So you could specify pre-conditions, post-conditions and invariants. When the code was compiled you could configure the compiler to generate or not generate code for these. And next to the support for the compiler, the pre- and post-conditions and invariants were also explicitly listed in the code documentation, and there was also a static analyzer that gave some hints/warnings or reported inconsistencies at compile-time. This was a project from a research team at Microsoft and we were aware of that (and that the libraries were not officially supported), but still sad to see it go. The code was made open-source, but was never really actively maintained. [0] Next to that, there is also the static analysis from JetBrains (ReSharper, Rider): you can use code annotations that are recognized by the IDE. It can be used for (simple) null/not-null analysis, but also more advanced stuff like indicating that a helper method returns null when its input is null (see the contract annotation). The IDE uses static analysis and then gives hints on where you can simplify code because you added null checks that are not needed, or where you should add a null-check and forgot it. I've noticed several times that this really helps and makes my code better and more stable. And I also noticed in code reviews bugs due to people ignoring warnings from this kind of analysis. And finally, in the Roslyn compiler, when you use nullable reference types, you get the null/not-null compile-time analysis. I wish the tools would go a lot further than this... [0] https://www.microsoft.com/en-us/research/project/code-contracts/ https://www.microsoft.com/en-us/research/project/code-contra... [1] https://www.jetbrains.com/help/resharper/Reference__Code_Annotation_Attributes.html#ContractAnnotationAttribute https://www.jetbrains.com/help/resharper/Reference__Code_Ann...
- jnash 4y ago
  There are tools and programming language that are already way ahead of what you are describing. Examples are Idris, F* (F-Star), Dafny etc. They use Dependent Types and/or Refinement Types to make it possible to prove your code correct. There is now proven correct code in the Windows Kernel and other large projects implemented with those tools.
fuzzythinker 4y ago
Nailed it. I see AI-coding is like hiring junior devs. It'll split out code fast, but unless carefully reviewed, it's just a means to push the tech debt forward. Which isn't bad in itself, as tech debt is good when companies understand the cost. But both are bad if there isn't a true understanding.
- snek_case 4y ago
  It's kind of like copying and pasting code from StackOverflow.. Except the code hasn't had as many eyes looking at it as something that was pasted on StackOverflow, and it has a higher likelihood of seeming like a correct solution to your specific use case. Honestly, it seems pretty dangerous. Seemingly correct code generated by a neural network that we think probably understands your code but may not. Easy to just autocomplete everything, accept the code as valid because it compiles, and discover problems at run-time.
- john_the_writer 4y ago
  Ha ha. I almost spit out my coffee. "when companies understand the cost". OMG that's hilarious.
indymike 4y ago
I think this requires a totally different approach to programming. The spec/proof/code cycle exists rarely in the real world. The AI generated code has the disadvantage of being trained on imperfect code, without having any context, so it's like an enthusiastic, very junior copy pasta coder.
- john_the_writer 4y ago
  Totally.
andrepd 4y ago
Hit the nail on the head. The major problem with NN is that they are completely unexplainable black boxes. The algorithm spits out a piece of code (or recommends clickbait videos, or bans you from a website, or denies you credit) based on a mishmash of assorted examples and a few million/billion parameters, but can neither explain why it picked it, nor verify that it is correct. Formal methods and theorem proving on the other hand, place a strong emphasis on proof production and verification.
jnash 4y ago
Yep 100% agree. And the good news is that we are moving closer every day to having tools that make proving code correct practical. Languages like Idris, Agda, Liquid Haskell, F* (F-star), LEAN etc. are spearheading this movement. If Rust had Refinement Types added it would turn it into a killer language for writing correct high performance code.
p1necone 4y ago
Isn't a sufficiently complete specification + proof with which to check generated code against just going to mean that a human spent exactly the same amount of time writing code as they would without the AI generation side of things?
- fdupress 4y ago
  Sure, but you get probably correct code out of it. Not every productivity increase has to do with quantity.
john_the_writer 4y ago
In all honesty, I typically spend almost twice as much time writing tests as I do writing the code that makes them pass. More often than not, once I have the tests written, the code nearly writes itself. There are edge cases when I have to look up things, but most of the time it's I'm happily TDD'ing.

YeGoblynQueenne 4y ago

>> I'd like to see better theorem proving, proof repair, refinement and specification synthesis. Thanks for making me smile. Some of us are working on exactly that kind of thing :)

qsort 4y ago

Can't +1 enough. This is clearly the future, as the increasing popularity of type systems shows. As interesting as those systems may be, they have it exactly backwards. Don't let the computer generate code and have the human check it for correctness: let the human write code and have the computer check it for correctness.

zozbot234 4y ago
> let the human write code and have the computer check it for correctness. Isn't that pretty much what ML does?
- goatlover 4y ago
  How would ML know what the correct code should be?
- kristjansson 4y ago
  That’s exactly the inverse of copilot and LLM code generation. The computer generates the code, the human checks if it’s correct
  - rmbyrro 4y ago
    I bet most humans won't check. See the mindset of the author: > ... I will not delve into the questions of code quality, security, legal & privacy issues, pricing, and others of similar character. ... Let’s just assume all this is sorted out and see what happens next.
john_the_writer 4y ago
Actually both don't work. The human also needs to make sure the code does what the Ticket asked for. And sometimes not even what the Ticket asked for, but what the business and user want/need. Honestly writing code is such a small part of a dev's job. It's figuring out how to translate the human (often non-tech) requirements into code that is also in a way that's also looking at requests that haven't been made yet.

monkeydust 4y ago

Machine readable specs? Something along lines of this perhaps... https://www.fixtrading.org/standards/fix-orchestra/ https://www.fixtrading.org/standards/fix-orchestra/

kimixa 4y ago
Aren't "Machine Readable Specs" a programming language?

galdosdi 4y ago

> It's not generating code that seems to be the difficulty, it's generating the correct code. Also, it's not actually writing the code that is the difficulty when generating code changes for maintaining existing code, but figuring out what changes need to be made to add up to the desired feature, and where in the codebase controls each of those, and possibly rediscovering important related invariants. For that matter, the really critical part of implementing a feature isn't implementing the feature -- it's deciding exactly what feature if any needs to be built! Even if many organizations try to split that among people who do and don't have the title of programmer (eg business analyst, product manager...), it's fundamentally programming and once you have a complex enough plan, even pushing around and working on the written English feature requirements resembles programming with some of the same tradeoffs. And we all know the nature of the job is that even the lowliest line programmer in the strictest agile process will still end up having to do some decision making about small details that end up impacting the user. Copilot is soooooo far away from even attempting to help with any of this, and the part it's starting with is not likely to resemble any of the other problems or contribute in any way to solving them. It's just the only part that might be at all tractable at the moment.

marcosdumay 4y ago

The unsettling part is that something like Copilot requires a lot of the work that would need to create an amazing semantic-aware linter like no other on the market. Instead, they decided to waste their work on that.

zokier 4y ago
> amazing semantic-aware linter like no other on the market. AWS has ML driven code analysis tools in their "CodeGuru" suite: https://aws.amazon.com/codeguru/ https://aws.amazon.com/codeguru/

rvdginste 4y ago

Exactly! A couple of years ago, we invested in using the libraries from Microsoft Code Contracts for a couple of projects. It was a really promising and interesting project. With the libraries you could follow the design-by-contract paradigm in your C# code. So you could specify pre-conditions, post-conditions and invariants. When the code was compiled you could configure the compiler to generate or not generate code for these. And next to the support for the compiler, the pre- and post-conditions and invariants were also explicitly listed in the code documentation, and there was also a static analyzer that gave some hints/warnings or reported inconsistencies at compile-time. This was a project from a research team at Microsoft and we were aware of that (and that the libraries were not officially supported), but still sad to see it go. The code was made open-source, but was never really actively maintained. [0] Next to that, there is also the static analysis from JetBrains (ReSharper, Rider): you can use code annotations that are recognized by the IDE. It can be used for (simple) null/not-null analysis, but also more advanced stuff like indicating that a helper method returns null when its input is null (see the contract annotation). The IDE uses static analysis and then gives hints on where you can simplify code because you added null checks that are not needed, or where you should add a null-check and forgot it. I've noticed several times that this really helps and makes my code better and more stable. And I also noticed in code reviews bugs due to people ignoring warnings from this kind of analysis. And finally, in the Roslyn compiler, when you use nullable reference types, you get the null/not-null compile-time analysis. I wish the tools would go a lot further than this... [0] https://www.microsoft.com/en-us/research/project/code-contracts/ https://www.microsoft.com/en-us/research/project/code-contra... [1] https://www.jetbrains.com/help/resharper/Reference__Code_Annotation_Attributes.html#ContractAnnotationAttribute https://www.jetbrains.com/help/resharper/Reference__Code_Ann...

jnash 4y ago
There are tools and programming language that are already way ahead of what you are describing. Examples are Idris, F* (F-Star), Dafny etc. They use Dependent Types and/or Refinement Types to make it possible to prove your code correct. There is now proven correct code in the Windows Kernel and other large projects implemented with those tools.

fuzzythinker 4y ago

Nailed it. I see AI-coding is like hiring junior devs. It'll split out code fast, but unless carefully reviewed, it's just a means to push the tech debt forward. Which isn't bad in itself, as tech debt is good when companies understand the cost. But both are bad if there isn't a true understanding.

snek_case 4y ago
It's kind of like copying and pasting code from StackOverflow.. Except the code hasn't had as many eyes looking at it as something that was pasted on StackOverflow, and it has a higher likelihood of seeming like a correct solution to your specific use case. Honestly, it seems pretty dangerous. Seemingly correct code generated by a neural network that we think probably understands your code but may not. Easy to just autocomplete everything, accept the code as valid because it compiles, and discover problems at run-time.
john_the_writer 4y ago
Ha ha. I almost spit out my coffee. "when companies understand the cost". OMG that's hilarious.

indymike 4y ago

I think this requires a totally different approach to programming. The spec/proof/code cycle exists rarely in the real world. The AI generated code has the disadvantage of being trained on imperfect code, without having any context, so it's like an enthusiastic, very junior copy pasta coder.

john_the_writer 4y ago
Totally.

andrepd 4y ago

Hit the nail on the head. The major problem with NN is that they are completely unexplainable black boxes. The algorithm spits out a piece of code (or recommends clickbait videos, or bans you from a website, or denies you credit) based on a mishmash of assorted examples and a few million/billion parameters, but can neither explain why it picked it, nor verify that it is correct. Formal methods and theorem proving on the other hand, place a strong emphasis on proof production and verification.

jnash 4y ago

Yep 100% agree. And the good news is that we are moving closer every day to having tools that make proving code correct practical. Languages like Idris, Agda, Liquid Haskell, F* (F-star), LEAN etc. are spearheading this movement. If Rust had Refinement Types added it would turn it into a killer language for writing correct high performance code.

p1necone 4y ago

Isn't a sufficiently complete specification + proof with which to check generated code against just going to mean that a human spent exactly the same amount of time writing code as they would without the AI generation side of things?

fdupress 4y ago
Sure, but you get probably correct code out of it. Not every productivity increase has to do with quantity.

john_the_writer 4y ago

In all honesty, I typically spend almost twice as much time writing tests as I do writing the code that makes them pass. More often than not, once I have the tests written, the code nearly writes itself. There are edge cases when I have to look up things, but most of the time it's I'm happily TDD'ing.