I’ve seen ChatGPT spit out both correct and incorrect code.
The idea that you’d rely more on tools is in a sense the Java approach. Java is somewhat more verbose than other languages, in practice, and you deal with the verbosity by making more use of code snippets / templates, autocompletion, etc. Basically, your IDE writes more of the code for you. I think this was, in general, a dead end in language research for various reasons, and improving code generation (via ChatGPT or some successor) does nothing to solve the actual problems with using generated code.
At the end of the day, somebody has to at least read the code and verify that it does what is requested.
Maybe at some point, someone will hook a more formal front-end to ChatGPT or something similar, so you can write the interfaces and specs, and the AI will generate the implementation. That may take a while, however.
> In Idris, types are a first class language construct, meaning that they can be manipulated and computed like any other language construct. It encourages a type-driven style of development, in which programmers give types first and use interactive editing tools to derive programs.
The idea that you’d rely more on tools is in a sense the Java approach. Java is somewhat more verbose than other languages, in practice, and you deal with the verbosity by making more use of code snippets / templates, autocompletion, etc. Basically, your IDE writes more of the code for you. I think this was, in general, a dead end in language research for various reasons, and improving code generation (via ChatGPT or some successor) does nothing to solve the actual problems with using generated code.
At the end of the day, somebody has to at least read the code and verify that it does what is requested.
Maybe at some point, someone will hook a more formal front-end to ChatGPT or something similar, so you can write the interfaces and specs, and the AI will generate the implementation. That may take a while, however.