AI generates test cases for its candidate functions, and computes their results
AI formally analyzes its candidate functions and looks for simple interesting guarantees it can make about their behavior
AI displays its candidate functions to the user, along with a summary of the test results and any guarantees about the input output behavior, and the user selects the one they want (which they can also edit, as necessary)
In this version, you go straight from English to code, which I think might be easier than from English to formal specification, because we have lots of examples of code with comments. (And I’ve seen demos of GPT-3 doing it for simple functions.)
I think some (actually useful) version of the above is probably within reach today, or in the very near future.
The workflow I’ve imagined is something like:
human specifies function in English
AI generates several candidate code functions
AI generates test cases for its candidate functions, and computes their results
AI formally analyzes its candidate functions and looks for simple interesting guarantees it can make about their behavior
AI displays its candidate functions to the user, along with a summary of the test results and any guarantees about the input output behavior, and the user selects the one they want (which they can also edit, as necessary)
In this version, you go straight from English to code, which I think might be easier than from English to formal specification, because we have lots of examples of code with comments. (And I’ve seen demos of GPT-3 doing it for simple functions.)
I think some (actually useful) version of the above is probably within reach today, or in the very near future.
Seems reasonable.