[vram22]

>I fully expect to see these tools start to become available over the next decade or so, given the current progress of program synthesis I see in the academic literature.

Interesting. I did know about program verification efforts (trying to prove that programs are correct), but had never heard of program synthesis (assuming it is somewhat different from code generation). Do you know of any examples of the kinds of areas it can be applied to?

[jcranmer]

The best overview of the topic I know of is https://www.microsoft.com/en-us/research/wp-content/uploads/..., which describes the state of the field ~18 months ago.

The major field where it's already being applied is in automating the conversion of data--building the program that can take "John Doe" and turn it into "<name>John</name> <surname>Doe</surname>" just by example. You can also do similar generalization to automate things like constructing highly repetitive graphics (e.g., draw a few teeth of a gear and the program does the rest). Superoptimization is the other main prong, where you really combine the synthesis and the verification to get correct faster code.

[vram22]

Those applications sound cool. Will check out that paper. Thanks.