5 ms·

Program Synthesis is Possible (2018)

98 points by xept 4y ago

LanternLight83 4y ago
First heard about program synthesis myself thanks to William Byrd's demo at the end of "The Most Beautiful Program[...]", https://youtu.be/OyfBQmvr2Hc https://youtu.be/OyfBQmvr2Hc @ 1:17:15
sanxiyn 4y ago
If you enjoyed this, it is possible that you may also enjoy this Rust port: https://fitzgeraldnick.com/2018/11/15/program-synthesis-is-possible-in-rust.html https://fitzgeraldnick.com/2018/11/15/program-synthesis-is-p....
_0ffh 4y ago
I recently considered using Z3 to solve an instruction scheduling problem but opted for a different approach in the end. I'd love to try Z3 for this some time in the future, but it seemed so much easier to implement a more pedestrian approach.
turnsout 4y ago
To clarify because it was non-obvious to me, this is program synthesis from mathematical formulae. I'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'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.
- mirker 4y ago
  Imagine building a compiler optimization pass. Do you want to hand-roll all the shifting equivalence relationships for division, etc?
- vivegi 4y ago
  Some examples of program synthesis. - Theorem proving: Being able to prove or disprove a mathematical statement based on axioms and other proven theorems. Eg: In formal software verification, building a program verifier based on the program's specification and source code or implementation. - Prolog Inference engine: Making inferences about logical statements based on other logical statements. Eg: deciding whether a user must be permitted or denied access to a resource based on various role assignments / group memberships. Another example would be the application of firewall rules.
lapinot 4y ago
The myth that program synthesis is hard and should be done using general-purpose tools like genetic/ml/smt has to die. Program synthesis is everywhere. 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 https://www.youtube.com/watch?v=brjFqXkUQv0 https://www.youtube.com/watch?v=brjFqXkUQv0 (in dependently typed language idris2). In fact when you squint, principled program synthesis is what compilers do: if your source language is a "mathematically clean language" (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. 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 "classical" programing language by a "meta-program".
- bjourne 4y ago
  > 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 "classical" programing language by a "meta-program". Can you give some examples? The high performance programs I know of are all written in either C, assembly, OpenCL, or hardware description languages.
  - andrepd 4y ago
    Fftw?
    - _0ffh 4y ago
      "Fastest Fourier Transform in The West" http://fftw.org/ http://fftw.org/
  - lapinot 4y ago
    Sure! So first, being in C/asm/.. is not incompatible with what i say: i'm saying that some of these are not hand-written, but are generated. So off the top of my head: - FFTW: an ocaml synthesizer for fft kernels from a fourier-transform DSL - basically all SQL engines, in particular the "query planner" part, which compiles an SQL query (functional spec based on the theory of relational algebra) into an imperative program (eg https://sqlite.org/opcode.html https://sqlite.org/opcode.html) - https://github.com/mit-plv/fiat-crypto https://github.com/mit-plv/fiat-crypto, verified crypto routines - https://www.flopoco.org/ https://www.flopoco.org/, float cores for fpga - https://faust.grame.fr/ https://faust.grame.fr/, audio synthesis from a functional stream-based language - tensorflow and other "static graph" neural-whatever-matrix-multiplication-libs (https://ocaml.xyz/tutorial/cgraph.html https://ocaml.xyz/tutorial/cgraph.html) - https://github.com/timelydataflow/differential-dataflow https://github.com/timelydataflow/differential-dataflow, incremental dataflow computations edit: i almost forgot all the openssl perl scripts, even if it can be seen more as macro-expansion than actual meta-programing/program synthesis: https://github.com/search?l=Perl&q=repo%3Aopenssl%2Fopenssl+path%3A%2Fcrypto&type=Code https://github.com/search?l=Perl&q=repo%3Aopenssl%2Fopenssl+... Basically all crypto libs use at least some form of compile-time execution to generate constants, offsets, tables, .. edit2: also svelte, a "virtual virtual" dom js thingy, never looked much into it, but afaik they do compile-time diffing, and thus generate imperative code (ie ugly old-school efficient spaghetti) from react-like vdom code.
DavidRogers0000 4y ago
jongjong 4y ago
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's obviously not since nobody seems to know what the heck they want these days. I've worked on so many software projects where the company director wanted things to be implemented a certain way, but once it'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'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. 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't require as thorough of an understanding of the domain.
- Tranny_bad 4y ago
- UncleMeat 4y ago
  I think this is overly pessimistic. A compiler isn't too different from a synthesis engine that is provided with formal specification. Virtually nobody says "writing code is the easy part so why are we having tools write our asm programs for us?" There is clearly a spectrum where the techniques can be valuable or harmful depending on where they are applied. "Hey, I synthesized a test case that will cover some uncovered program path", "hey, I synthesized some parser based on some yacc specification", and "hey, I synthesized a network topology that will break the moment requirements change" are all synthesis but have various degrees of unintentional impact.

98 points by xept 4y ago

First heard about program synthesis myself thanks to William Byrd's demo at the end of "The Most Beautiful Program[...]", https://youtu.be/OyfBQmvr2Hc https://youtu.be/OyfBQmvr2Hc @ 1:17:15

sanxiyn 4y ago

If you enjoyed this, it is possible that you may also enjoy this Rust port: https://fitzgeraldnick.com/2018/11/15/program-synthesis-is-possible-in-rust.html https://fitzgeraldnick.com/2018/11/15/program-synthesis-is-p....

_0ffh 4y ago

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

turnsout 4y ago

To clarify because it was non-obvious to me, this is program synthesis from mathematical formulae. I'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'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.

mirker 4y ago
Imagine building a compiler optimization pass. Do you want to hand-roll all the shifting equivalence relationships for division, etc?
vivegi 4y ago
Some examples of program synthesis. - Theorem proving: Being able to prove or disprove a mathematical statement based on axioms and other proven theorems. Eg: In formal software verification, building a program verifier based on the program's specification and source code or implementation. - Prolog Inference engine: Making inferences about logical statements based on other logical statements. Eg: deciding whether a user must be permitted or denied access to a resource based on various role assignments / group memberships. Another example would be the application of firewall rules.

lapinot 4y ago

The myth that program synthesis is hard and should be done using general-purpose tools like genetic/ml/smt has to die. Program synthesis is everywhere. 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 https://www.youtube.com/watch?v=brjFqXkUQv0 https://www.youtube.com/watch?v=brjFqXkUQv0 (in dependently typed language idris2). In fact when you squint, principled program synthesis is what compilers do: if your source language is a "mathematically clean language" (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. 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 "classical" programing language by a "meta-program".

bjourne 4y ago
> 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 "classical" programing language by a "meta-program". Can you give some examples? The high performance programs I know of are all written in either C, assembly, OpenCL, or hardware description languages.
- andrepd 4y ago
  Fftw?
  - _0ffh 4y ago
    "Fastest Fourier Transform in The West" http://fftw.org/ http://fftw.org/
- lapinot 4y ago
  Sure! So first, being in C/asm/.. is not incompatible with what i say: i'm saying that some of these are not hand-written, but are generated. So off the top of my head: - FFTW: an ocaml synthesizer for fft kernels from a fourier-transform DSL - basically all SQL engines, in particular the "query planner" part, which compiles an SQL query (functional spec based on the theory of relational algebra) into an imperative program (eg https://sqlite.org/opcode.html https://sqlite.org/opcode.html) - https://github.com/mit-plv/fiat-crypto https://github.com/mit-plv/fiat-crypto, verified crypto routines - https://www.flopoco.org/ https://www.flopoco.org/, float cores for fpga - https://faust.grame.fr/ https://faust.grame.fr/, audio synthesis from a functional stream-based language - tensorflow and other "static graph" neural-whatever-matrix-multiplication-libs (https://ocaml.xyz/tutorial/cgraph.html https://ocaml.xyz/tutorial/cgraph.html) - https://github.com/timelydataflow/differential-dataflow https://github.com/timelydataflow/differential-dataflow, incremental dataflow computations edit: i almost forgot all the openssl perl scripts, even if it can be seen more as macro-expansion than actual meta-programing/program synthesis: https://github.com/search?l=Perl&q=repo%3Aopenssl%2Fopenssl+path%3A%2Fcrypto&type=Code https://github.com/search?l=Perl&q=repo%3Aopenssl%2Fopenssl+... Basically all crypto libs use at least some form of compile-time execution to generate constants, offsets, tables, .. edit2: also svelte, a "virtual virtual" dom js thingy, never looked much into it, but afaik they do compile-time diffing, and thus generate imperative code (ie ugly old-school efficient spaghetti) from react-like vdom code.

DavidRogers0000 4y ago

jongjong 4y ago

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's obviously not since nobody seems to know what the heck they want these days. I've worked on so many software projects where the company director wanted things to be implemented a certain way, but once it'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'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. 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't require as thorough of an understanding of the domain.

Tranny_bad 4y ago
UncleMeat 4y ago
I think this is overly pessimistic. A compiler isn't too different from a synthesis engine that is provided with formal specification. Virtually nobody says "writing code is the easy part so why are we having tools write our asm programs for us?" There is clearly a spectrum where the techniques can be valuable or harmful depending on where they are applied. "Hey, I synthesized a test case that will cover some uncovered program path", "hey, I synthesized some parser based on some yacc specification", and "hey, I synthesized a network topology that will break the moment requirements change" are all synthesis but have various degrees of unintentional impact.