How is program synthesis better than writing code?

[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/asdfa2342543]

I don’t think anyone’s really claiming that it’s easier.  But it has the advantage of provable correctness, some kind of optimizer could find an optimal implementation. 

I could also see higher level things being easier to reason about correctly.  

[u/BuyerImpressive4325 → u/asdfa2342543]

But that correctness assumes that the spec sheet itself is correct? Isn’t that identical in that the spec sheet has to be written perfectly?

[u/asdfa2342543 → u/BuyerImpressive4325]

Yes… from an information theory perspective, you need to give the program the information one way or another. But when you foreground the constraints instead of the implementation, it requires less searching though the codebase and “manually” identifying and combining those constraints. 

You could say you’re making local reasoning a little bit harder in exchange for easier global reasoning.  

[u/4xe1 → u/BuyerImpressive4325]

Just like it's easier to check that an array is sorted than to actually sort it, it's easier to specify that an array ought to be sorted. The spec sheet also describes what you want, which you presumably already know, unlike how you want it. So the spec is much easier to get right.

In trivial examples, constraints are an equally complex version of writing the code, but for more complex ones, specs beat code. The place where constraints get really tedious is when the constraints are not enough for the synthetizer to find a solution, and you have to encode intermediate steps, but if you get them wrong, you will realize it.

[u/rarely_lewd_bases → u/asdfa2342543]

the spec doesn't have to worry about implementation details leaking in, that's the whole point. you can describe what you want without even knowing which language it'll end up in, and the synthesizer can pick a version that's optimized for speed or memory depending on the target. writing the code yourself means you're already making those tradeoffs before you've even tested the logic

[u/charolastrauno]

Presumably you also get a proof that the program obeys the specification from the synthesis process. No one is stopping you from writing all three yourself though!

[u/BuyerImpressive4325 → u/charolastrauno]

But doesn’t that just shift the issue, instead of checking if the program was written correctly, you instead need to check if the spec sheet was correct?

[u/omega1612 → u/BuyerImpressive4325]

You always need to verify it. Otherwise what's the use of the spec?

[u/BuyerImpressive4325 → u/omega1612]

But if you need to verify the spec sheet, and the spec sheet is just as complex, doesn’t that mean that it has the same risk of failure? What’s the difference?

[u/charolastrauno → u/BuyerImpressive4325]

A spec is meant to be higher level and “more obvious” for a human to check than trying to check a program.

[u/omega1612 → u/BuyerImpressive4325]

Originally you had two problems:

1) is this spec right? Does it reflects what I want?

2) Does this program follows the spec?

Combined they answer another question:

Does the program does what I want/need?

Just from formal theory, it is impossible in general to answer the question (reduce it to the halting problem to see it).

The split in two questions is a way to split the responsibilities. The first questions captures the difficulty of formalizing the needs. Or in more common jargon "is my architecture right? Does my model really models the original domain? Does it contains some error?"

The issue is that the problems to solve by a program are often expressed and understood in a natural language full of ambiguity and totally dependent on the context. So, while we can try to minimize the issues in that area, is till a widely open problem.

[u/astrolabe]

For a lot of algorithms, the problem solved is simpler than the algorithm itself. For example, the simplex algorithm for linear programming, or the hungarian algorithm for the auction problem, or the A* algorithm for finding the shortest route. I'm sure I could go on.

[u/donaldhobson]

For some problems, it's easy to specify a constraint like "if you encrypt a file, and then decrypt it again, the result should always be exactly the same".

But that sort of constraint isn't easy to program in when writing a normal encryption algorithm.

[u/kchanqvq]

It generates research papers and funding, just writing the code wouldn't.

[u/Samrockswin → u/kchanqvq]

To be a little less glib, the issues with program synthesis is eventually you need to synthesize something that is outside of the capabilities of your synthesizer so you end up having.

That said, done well program synthesis can be very powerful. If you know you need some sort of tensor operation. There's been a lot of success if there's a good abstraction between interface and implementation, which is often the case in a lot of the ML work in the past decade. But in other cases the spec gets just as complicated as the implementation and the benefits of program synthesis is lessened. I've been running into a similar issue with domain specific languages too; eventually, the DSL doesn't have the weird thing you need (debugger, foreign function interface, whatever) and you are either stuck or have to do some arcane workaround.