Live data from Hacker News

Show HN: Program Synthesis for Ruby

github.com

1–10 of 20 posts

Re: Show HN: Program Synthesis for Ruby

#2
> 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.

Re: Show HN: Program Synthesis for Ruby

#3

> 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…

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

Re: Show HN: Program Synthesis for Ruby

#4
post #3

> 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…

> 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 ne…

> You still write the tests in standard Ruby and synthesized code should satisfy the logic as checked by the tests.

I think its important that the code still be user-modifiable:

Take this function, y = 2 * x.

Write a test, which proves for all real numbers, that y = 2 * x.

Can't do it, can you?

Tests can't fully specify code - this effort is doomed to be incomplete.

Re: Show HN: Program Synthesis for Ruby

#5
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.

Re: Show HN: Program Synthesis for Ruby

#6
post #5

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 issu…

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).

Re: Show HN: Program Synthesis for Ruby

#7

> 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…

> 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..? :|

Re: Show HN: Program Synthesis for Ruby

#8
post #3

> 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…

> 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 ne…

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.

Re: Show HN: Program Synthesis for Ruby

#9
post #8
post #3

Earlier quoted context omitted.

> 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 ne…

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.

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.

Re: Show HN: Program Synthesis for Ruby

#10
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?
Post reply on HN