[HN Gopher] Show HN: Program Synthesis for Ruby
___________________________________________________________________
Show HN: Program Synthesis for Ruby
Author : sankha93
Score : 73 points
Date : 2022-04-13 14:52 UTC (8 hours ago)
(HTM) web link (github.com)
(TXT) w3m dump (github.com)
| noneeeed wrote:
| Interesting. Reminds me of my time at university using something
| called Progol. You gave it positive and negative cases and it's
| algorithm would (very slowly) try and come up with Prolog code
| that fit it.
|
| It was an interesting idea but in reality we spent so much time
| having to spoon-feed it more and more carefully constructed
| examples that it just seemed pointless.
|
| Not to say that this will suffer from the same issue, but I do
| wonder if the benefit will really be significant enough to make
| it worth it.
| sankha93 wrote:
| Indeed, there is rich prior work on example based program
| synthesis. Often these use inductive logic programming or aided
| by SMT solvers if these examples can be lifted to solver level
| values (think integers or booleans, or data types made from
| those).
|
| However, not all program values can be easily lifted to
| solvers. So the goal with RbSyn is to allow the programmer to
| write the same tests they would have written anyway to check
| their program correctness, without any extra fiddling. As tests
| subsume examples, we expect more program behavior can be
| specified than just using simple examples.
|
| > I do wonder if the benefit will really be significant enough
| to make it worth it.
|
| I have often pondered on what makes a program synthesis tool
| useful. I expect writing code as art as much as it is science,
| and people like to express code in the way they model system
| behavior in their head. In that regard, I do not think program
| synthesis tools will enable you to automate away large parts of
| code, but I do think it will automate mundane parts of a
| program; like writing utility methods, or filling in a partial
| program when enough information can be gathered from
| surrounding context (such as the arguments you write for a
| substring function).
| pmontra wrote:
| I'm writing a Rails API app (for a customer) that is a client to
| Alexa's Skill Management API and is a server for a backend app. I
| have tests but I'm afraid that without a 100% coverage of all
| corner cases I'll be disappointed by some results and it could be
| difficult to manually fix the code generated by the program. Am I
| overly pessimistic?
| eatonphil wrote:
| > Given a method specification in the form of tests, type and
| effect annotations with RDL, this synthesizes a Ruby function
| that will pass the tests. This reduces programmer effort to just
| writing tests that specify the function behavior and the computer
| writing the function implementation for you.
|
| That's really neat! But doesn't this just mean that instead of
| writing your code and logic in Ruby you're writing it in RDL?
|
| Also, it would be great to see some examples in the README or in
| an examples folder. It's kind of hard for me to tell exactly what
| I need to write and what to call to generate the Ruby.
| bingo-bongo wrote:
| > But doesn't this just mean that instead of writing your code
| and logic in Ruby you're writing it in RDL?
|
| ..and write a test for it..? :|
| sankha93 wrote:
| > But doesn't this just mean that instead of writing your code
| and logic in Ruby you're writing it in RDL?
|
| RDL allows the specification of types and effect labels only.
| You still write the tests in standard Ruby and synthesized code
| should satisfy the logic as checked by the tests.
|
| > Also, it would be great to see some examples in the README or
| in an examples folder. It's kind of hard for me to tell exactly
| what I need to write and what to call to generate the Ruby.
|
| Sorry for the sparse documentation, I plan to improve that. I
| have added an example to the readme. Other examples can be
| found in `test/benchmark` folder.
| smaudet wrote:
| evolve2k wrote:
| It would be wonderful if you could embed a short video that
| explains the concept and shows some practical examples.
|
| What it can do now. What are the limits. What's planned next?
| Are questions we have as first time visitors.
| sankha93 wrote:
| Thanks for the feedback! I just uploaded a video now that
| demos RbSyn in action:
| https://www.youtube.com/watch?v=yYAOK5S8lRY
|
| The concepts, capabilities, and limitations of RbSyn are
| explained in this talk:
| https://www.pldi21.org/poster_pldi.124.html with full
| details in the accompanying PLDI paper:
| https://arxiv.org/abs/2102.13183
|
| I will link these from the readme soon.
___________________________________________________________________
(page generated 2022-04-13 23:01 UTC)