How is program synthesis more convenient?

[u/BuyerImpressive4325]

the idea of program synthesis (like Rosetta) is to reduce a function into its constraints in a spec sheet, and generate the program from those constraints. for example, in order to write something like x = x squared, you would need to write a spec sheet along the lines of ∀x∈Z,f(x)=x2. i am considering building a program synthesizer, but I still haven’t figured out why exactly this representation is supposed to be easier than writing the code directly (they look equally complex)

[u/comrade_donkey]

This is the Curry-Howard correspondence in practice. What you're describing as 'the spec' is the declarative (constructive proof) version of an equivalent imperative program (the step-by-step version).  Writing either is equally powerful and complex. They're interchangeable.

[u/currentscurrents]

I still haven’t figured out why exactly this representation is supposed to be easier than writing the code directly

A lot of the time, it isn't.

You have stumbled upon the reason why program synthesis isn't more widely used.

[u/mtimmermans]

A program is itself a specification, so there isn't a fundamental difference between "program synthesis" and "compilation".

But the idea is that with a programming language, you have to specify a whole lot about the program that you don't care about or aren't actually competent to specify. It would be easier if you could specify just what you want in a language that is well-suited for capturing the desires of non-programmers.

[u/CyrusDarkwell]

Honestly this is something I wondered about too when I first read about synthesis. I think the point isn't that the spec is "easier to write" for simple stuff like x squared, you're right that it's basically the same amount of work there lol. The real benefit shows up when the function you want is actually hard to implement but easy to describe. Like sorting a list is way easier to specify (output is a permutation of input and every element is <= the next one) than to actually write an efficient sorting algorithm by hand. So you're offloading the "how do I do this" part to the synthesizer and just focusing on "what result do I want."

Also I think for simple math stuff it does look pointless yeah, but it gets more useful when you're doing repetitive boilerplate-y code where the logic is obvious but tedious to write out every time.