6 ms·
Some amazing progress is being made in the field of program synthesis. In particular, there have been a lot of successes in generating programs from input/outpu
by wsxcde 11y ago
Some amazing progress is being made in the field of program synthesis. In particular, there have been a lot of successes in generating programs from input/output examples, provided the domain is sufficiently restrictive and/or the programmer provides a "sketch" or partial program to start off the synthesizer with. One good paper to start looking at is: Oracle guided program synthesis, Jha and others ICSE'10. This algorithm has made its way into Microsoft Excel: http://research.microsoft.com/en-us/news/features/flashfill-020613.aspx http://research.microsoft.com/en-us/news/features/flashfill-....
You might argue this isn't "true" program synthesis, but in some cases it can outdo human programs, because the synthesizer can be tied into a verifier to produce only "correct" programs, where correctness is defined by a few simple and declarative properties. One example of this sort of thing is from Udupa and colleagues in PLDI'13: http://dl.acm.org/citation.cfm?doid=2462156.2462174 http://dl.acm.org/citation.cfm?doid=2462156.2462174. They're able to generate correct cache coherence protocols from a partial specification and input/output examples. This is a big improvement over the current state of the art, where a lot of very smart people think really hard and come up with a coherence protocol, convince themselves it's correct, and then some other very smart people spend a few months playing with automated verifiers trying to prove the protocol correct, and finally someone actually implements the protocol in hardware, and you might still run into bugs at this stage.