4 ms·

> given a fully or mostly-specified definition of some function foo, Barliman will attempt to prove that a partially-specified test is consistent with, or incon

by runeks 10y ago

> given a fully or mostly-specified definition of some function foo, Barliman will attempt to prove that a partially-specified test is consistent with, or inconsistent with, the definition of foo. I feel like this is what GHC (the Haskell compiler) does for me. Where the "test", in this case, is the type definition. And there is no room for error here. So it's possible that this idea makes more sense for languages without a strong type system. In any case, trying to complete a partial function definition without looking at the native types of the language means you miss a lot of information, especially in the case of Haskell, where the types tell you so much, if not everything, you need to know about a function.

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 ago
    Hopefully 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...
will_byrd 10y ago
Thank you for your comments! I agree that type-directed synthesis would be very helpful. One of the inspirations for Barliman is the type-and-example-directed program synthesis by Peter-Michael Osera and Steve Zdancewic: http://www.cis.upenn.edu/~stevez/papers/OZ15.pdf http://www.cis.upenn.edu/~stevez/papers/OZ15.pdf I want to experiment with a typed version of Scheme (a mini-ML with s-expressions) to see how much types would improve synthesis. In previous work with Michael Ballantyne, Michael showed that adding types could significantly improve the synthesis capability of the relational interpreter used by Barliman. The miniKanren constraint logic system used by Barliman can be use to write type checkers and type inferencers that can perform type habitation, similar in spirit to the Djinn system mentioned by Cybiote. This is a topic Oleg Kiselyov and Dan Friedman have explored, for example. I'm very interested in improving our ability to write more sophisticated type inferencers in miniKanren, and in using the inferencer to guide synthesis. Part of the motivation for Barliman is to explore what can be done for dynamically typed languages. Perhaps something like soft typing or gradual typing would be useful in this context. Another idea I want to explore is using high-level properties, as in property-based testing, or even software contracts, to help guide synthesis. I should mention that Greg Rosenblatt has improved Barliman's synthesis abilities recently, by specializing the underlying relational interpreter, using techniques similar to those in the Mercury compiler. I need to update the documentation to show the improved synthesis, which still needs work in order to be useful. I'm also working with Rob Zinkov and Evan Donahue on using stochastic search to improve miniKanren's synthesis ability. I'm very much open to collaboration on Barliman, synthesis, relational interpreters/type inferencers, constraint logic programming, etc.
- runeks 10y ago
  I guess I don't quite understand the root purpose of program synthesis. It's my impression, as a programmer, that the difficult task is defining ones program logic without ambiguity. If this is indeed the case, then program synthesis already exists in the form of Coq, but it doesn't mean we've made programming easier, it means we've created a tool that reveals all possible failure points of a program, forcing us to consider all possible outcomes. It makes for a provably un-crashable program, but we pay for it in the time it takes to create the specification/implementation (which at this point have converged into one). If I can write a specification in a language that some tool can transform into a source code implementation (which can then be compiled and executed), then I wouldn't call that tool a "program synthesizer" but rather a "compiler" (and the specification language would then be a programming language).

by runeks 10y ago

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 ago
  Hopefully 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...

will_byrd 10y ago

Thank you for your comments! I agree that type-directed synthesis would be very helpful. One of the inspirations for Barliman is the type-and-example-directed program synthesis by Peter-Michael Osera and Steve Zdancewic: http://www.cis.upenn.edu/~stevez/papers/OZ15.pdf http://www.cis.upenn.edu/~stevez/papers/OZ15.pdf I want to experiment with a typed version of Scheme (a mini-ML with s-expressions) to see how much types would improve synthesis. In previous work with Michael Ballantyne, Michael showed that adding types could significantly improve the synthesis capability of the relational interpreter used by Barliman. The miniKanren constraint logic system used by Barliman can be use to write type checkers and type inferencers that can perform type habitation, similar in spirit to the Djinn system mentioned by Cybiote. This is a topic Oleg Kiselyov and Dan Friedman have explored, for example. I'm very interested in improving our ability to write more sophisticated type inferencers in miniKanren, and in using the inferencer to guide synthesis. Part of the motivation for Barliman is to explore what can be done for dynamically typed languages. Perhaps something like soft typing or gradual typing would be useful in this context. Another idea I want to explore is using high-level properties, as in property-based testing, or even software contracts, to help guide synthesis. I should mention that Greg Rosenblatt has improved Barliman's synthesis abilities recently, by specializing the underlying relational interpreter, using techniques similar to those in the Mercury compiler. I need to update the documentation to show the improved synthesis, which still needs work in order to be useful. I'm also working with Rob Zinkov and Evan Donahue on using stochastic search to improve miniKanren's synthesis ability. I'm very much open to collaboration on Barliman, synthesis, relational interpreters/type inferencers, constraint logic programming, etc.

runeks 10y ago
I guess I don't quite understand the root purpose of program synthesis. It's my impression, as a programmer, that the difficult task is defining ones program logic without ambiguity. If this is indeed the case, then program synthesis already exists in the form of Coq, but it doesn't mean we've made programming easier, it means we've created a tool that reveals all possible failure points of a program, forcing us to consider all possible outcomes. It makes for a provably un-crashable program, but we pay for it in the time it takes to create the specification/implementation (which at this point have converged into one). If I can write a specification in a language that some tool can transform into a source code implementation (which can then be compiled and executed), then I wouldn't call that tool a "program synthesizer" but rather a "compiler" (and the specification language would then be a programming language).