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.
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.
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.
Isn't that pretty much what ML does?
> ... 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.
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.
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.
Formal methods and theorem proving on the other hand, place a strong emphasis on proof production and verification.
Instead, they decided to waste their work on that.
AWS has ML driven code analysis tools in their "CodeGuru" suite: https://aws.amazon.com/codeguru/
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.
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-contra... [1] https://www.jetbrains.com/help/resharper/Reference__Code_Ann...
Thanks for making me smile. Some of us are working on exactly that kind of thing :)
Something along lines of this perhaps...