Isn't this how copilot 'just' works, except with comments? What's the advantage over copilot?
you get to delay code review
Maccarone: AI-managed code blocks in Python
41–50 of 75 posts
Re: Maccarone: AI-managed code blocks in Python
#42In theory, an AI that wrote proofs for their code (ala coq) could be used to validate preconditions specified by the developer, right?
I don't know to what extent you can self-verify your own system based on proof code you also write yourself. However I do know this topic of merging AI, Deep Learning, and proof assistants is an up and coming research area. I mainly follow publications from Talia Ringer [1] and collaborators on this topic. [1] https://dependenttyp.es/
Maybe I misunderstand, but my understanding is that (at least some languages) can be given proofs of correctness for some pre and post conditions. See e.g., https://arxiv.org/pdf/2303.05491.pdf
Conceptually, you tell the computer how to validate that the conditions you state are correct with your proof, and it checks that each step follows.
Re: Maccarone: AI-managed code blocks in Python
#43How hard would it be to use code llama instead? https://ai.meta.com/blog/code-llama-large-language-model-cod...
Re: Maccarone: AI-managed code blocks in Python
#44Earlier quoted context omitted.
We, as an industry, didn't stop shipping bugs. (Small example: https://github.com/CVEProject/cvelistV5/releases ) And that thorough code review prevents bugs is, at best, a debatable assertion. See e.g. https://www.microsoft.com/en-us/research/publication/code-re... It finds _some_ bugs. CI/CD, and a massive investment in automated testing has probably had the largest impact in moving software quality forward. (See e…
The parent comment is sarcastic
Sorry I thought that was too obvious to warrant an /s but I suppose not.
Re: Maccarone: AI-managed code blocks in Python
#45Earlier quoted context omitted.
I don't know to what extent you can self-verify your own system based on proof code you also write yourself. However I do know this topic of merging AI, Deep Learning, and proof assistants is an up and coming research area. I mainly follow publications from Talia Ringer [1] and collaborators on this topic. [1] https://dependenttyp.es/
Maybe I misunderstand, but my understanding is that (at least some languages) can be given proofs of correctness for some pre and post conditions. See e.g., https://arxiv.org/pdf/2303.05491.pdf Conceptually, you tell the computer how to validate that the conditions you state are correct with your proof, and it checks that each step follows.
To me, it seems like there will be a finite set of pre and post conditions ever needed for 99% of future programming, and eventually everything will be a catalog of the conditions to working code.
One just needs a language to write those conditions in.
Re: Maccarone: AI-managed code blocks in Python
#46Very cool project. How reliable are you finding your prompts? They look like good choices based on my experience prompting GPT-3.5 and 4 for code editing. FYI, I think my open source tool aider would work out of the box to serve this use case. You would just run: aider file.py —msg “implement the comments” Of course aider works with any popular language, not just python. And it can do a lot of other coding tasks. It'…
Paul's work on this problem space is worth following, or at least reading the thoughts and iterative engineering results such as this comparison of the GPT models and the new functions API:
Re: Maccarone: AI-managed code blocks in Python
#47Looks amazing. Would you ever consider using Claude as well?
I prefer to use Claude for code generation if using a newer framework or language (the 2021 cutoff with gpt-4 is unfortunate)
Re: Maccarone: AI-managed code blocks in Python
#48Very cool project. How reliable are you finding your prompts? They look like good choices based on my experience prompting GPT-3.5 and 4 for code editing. FYI, I think my open source tool aider would work out of the box to serve this use case. You would just run: aider file.py —msg “implement the comments” Of course aider works with any popular language, not just python. And it can do a lot of other coding tasks. It'…
I absolutely love aider and tell everyone I run into about it. Keep it the great work!
Question: can aider work with Ooba/llama.CPP/meta code llama on local llm? If not yet, are you planning on it?
So many users just can’t use GPT4/Copilot because of corporate policy. But they have Macs with M2.
Re: Maccarone: AI-managed code blocks in Python
#49> What prevents my program from behaving differently after each preprocessing run?
>The strength of your faith in GPT-4.
I got a chuckle out of that
Re: Maccarone: AI-managed code blocks in Python
#50In theory, an AI that wrote proofs for their code (ala coq) could be used to validate preconditions specified by the developer, right?
Reflexion can serve as good reference here:
https://arxiv.org/abs/2303.11366
Essentially, AI’s output is fed into a checker, whose output is fed back into the AI for “reflexion”. Then the AI often corrects (leading to noticeable improvement in GPT-4 perf).