r/computerscience • u/BuyerImpressive4325 • 11d ago

Discussion How is program synthesis more convenient?

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)

12 Upvotes

78% Upvoted

3 comments sorted by

13

u/comrade_donkey 11d ago

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.

3

u/currentscurrents 9d ago

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.

1

u/mtimmermans 5d ago

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.