> where I think you meant to say "a valid specification". Did I misunderstand? What do you mean when you say "a valid specification"? There are known algorithm

> where I think you meant to say "a valid specification". Did I misunderstand? What do you mean when you say "a valid specification"? There are known algorithms to check validity of a proof. How do you check that specification is valid? People are inspecting it and agree that "yes, it seems to be expressing what was intended to be expressed in the natural language", or, "no, this turn of phrase needs to be understood in a different way" or some such. Today there's no other system that can handle this kind of a task besides humans (who are fallible) and LLMs (that are much more fallible). That is deciding that specification is valid cannot be done without human involvement. I left that part out and focused on what we can mechanistically check (that is validity of a proof). So, no, I didn't mean "a valid specification". And, yes, I don't think that today's LLMs would be good at producing specifications that would be deemed valid by a consensus of experts. > Today, if you can express your problem in terms of input-output examples there are approaches that can synthesize a program that is consistent with the examples In a limited domain with agreed-upon rules of generalization? Sure. In general? No way. The problem of generalizing from a limited number of examples with no additional restrictions is ill-defined. And the problem "generalize as an expert would do" is in the domain of AI.