3 ms·
I don't think that is quite right. This says it's applying basic ideas from program synthesis, which is not too distant from automated theorem proving style AI
by Cybiote 10y ago
I don't think that is quite right. This says it's applying basic ideas from program synthesis, which is not too distant from automated theorem proving style AI (specially when you get to SMT solver based synthesis).
From skimming the page, it looks to me like an example of inductive programming.
So for Haskell, it would be closer to something like Djinn, where code is generated/proved from a type specification.
- runeks 10y ago> So for Haskell, it would be closer to something like Djinn, > where code is generated/proved from a type specification. I don't understand. How is this generating/proving different, in essence, from GHC generating machine code from Haskell? What do we gain by having Djinn generate the Haskell code, rather than writing the Haskell ourselves?
- will_byrd 10y agoHopefully my answer above makes this more clear. The high-level idea is that if you are going to take the trouble to specify the type of a function (as in Haskell), and tests that use the function (as in unit testing), and high-level properties of the function (as in Quickcheck), you may as well try to get the computer to actually generate the function for you, rather than writing it yourself. You mentioned Coq above. Coq users rely on the `crush` tactic to try to fill in the boring details of a proof obligation. This is similar in spirit to search used in synthesis systems. If you can give the high-level specification, let the computer do the "boring" work. Of course, the boring work may be difficult or computationally expensive, and the high-level specification may be ambiguous...