Program Synthesis is Possible (2018)

The myth that program synthesis is hard and should be done using general-purpose tools like genetic&#x2F;ml&#x2F;smt has to die. Program synthesis is everywhere.<p>Program synthesis is far more tractable (as in, with complete or otherwise principled solvers and not ad-hoc SMT) in languages with strong or precise typing, eg <a href="https:&#x2F;&#x2F;www.youtube.com&#x2F;watch?v=brjFqXkUQv0" rel="nofollow">https:&#x2F;&#x2F;www.youtube.com&#x2F;watch?v=brjFqXkUQv0</a> (in dependently typed language idris2). In fact when you squint, principled program synthesis is what compilers do: if your source language is a &quot;mathematically clean language&quot; (eg regex, functional, dsl, ..), you can view your source program actually as a specification and the compiled output as a synthesized program validating that specification.<p>Several of high-performance programs are already written this way: crypto assembly routines, scientific kernels, sql queries, etc: they are written in a specific dsl which is closer to a mathematical spec than an algorithm, and then they are compiled to a &quot;classical&quot; programing language by a &quot;meta-program&quot;.

To clarify because it was non-obvious to me, this is program synthesis from mathematical formulae.<p>I&#x27;m curious what problems this solves, and in which domains this would be most useful. In the places where I see a lot of formula (computer graphics and ML papers), it doesn&#x27;t seem like the authors have a hard time implementing the algorithm from the math—in fact, the algorithm may have come first in some cases.

If you enjoyed this, it is possible that you may also enjoy this Rust port: <a href="https:&#x2F;&#x2F;fitzgeraldnick.com&#x2F;2018&#x2F;11&#x2F;15&#x2F;program-synthesis-is-possible-in-rust.html" rel="nofollow">https:&#x2F;&#x2F;fitzgeraldnick.com&#x2F;2018&#x2F;11&#x2F;15&#x2F;program-synthesis-is-p...</a>.

First heard about program synthesis myself thanks to William Byrd&#x27;s demo at the end of &quot;The Most Beautiful Program[...]&quot;, <a href="https:&#x2F;&#x2F;youtu.be&#x2F;OyfBQmvr2Hc" rel="nofollow">https:&#x2F;&#x2F;youtu.be&#x2F;OyfBQmvr2Hc</a> @ 1:17:15

The issue I have with program synthesis is the same issue as I have with no-code tools; writing code is the easy part of software development. The hard part is understanding precisely what the stakeholders really want. It sounds trivial, yet it&#x27;s obviously not since nobody seems to know what the heck they want these days.<p>I&#x27;ve worked on so many software projects where the company director wanted things to be implemented a certain way, but once it&#x27;s implemented that way, they suddenly realize that it (necessarily) affects some other functionality in a way that they did not anticipate... Then they decide they want it done another way; this kind of back-and-forth thinking process also happens when coding except it&#x27;s more granular (and usually you try to foresee the tradeoffs before you start to implement the solution; since the tradeoffs should affect your choice of solution). Every decision counts and relates back to the requirements; AI could not generate good code unless it had a human-level understanding of the problem and requirements.<p>Coding is about precise decision-making. It would be easier for AI to replace managers and executives since these roles involve far less precise decision-making and they don&#x27;t require as thorough of an understanding of the domain.

I recently considered using Z3 to solve an instruction scheduling problem but opted for a different approach in the end. I&#x27;d <i>love</i> to try Z3 for this some time in the future, but it seemed so much easier to implement a more pedestrian approach.