Program Synthesis is Possible (2018)(cs.cornell.edu)
cs.cornell.edu
Program Synthesis is Possible (2018)
https://www.cs.cornell.edu/~asampson/blog/minisynth.html
16 comments
> 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.
Can you give some examples? The high performance programs I know of are all written in either C, assembly, OpenCL, or hardware description languages.
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://github.com/mit-plv/fiat-crypto, verified crypto routines
- https://www.flopoco.org/, float cores for fpga
- 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://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+... 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.
- 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://github.com/mit-plv/fiat-crypto, verified crypto routines
- https://www.flopoco.org/, float cores for fpga
- 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://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+... 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.
remark: i've included some in the list (i believe sqlite, timelydataflow) which are doing the program synthesis at runtime (in contrast with the other that really output some kind of library that you bind to afterwards). These might more be qualified as staged computations. In general, "staged computation" is a good keyword to search for these things.
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.
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.
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.
- 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.
Imagine building a compiler optimization pass. Do you want to hand-roll all the shifting equivalence relationships for division, etc?
If you enjoyed this, it is possible that you may also enjoy this Rust port: https://fitzgeraldnick.com/2018/11/15/program-synthesis-is-p....
First heard about program synthesis myself thanks to William Byrd's demo at the end of "The Most Beautiful Program[...]", https://youtu.be/OyfBQmvr2Hc @ 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'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.
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.
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.
"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.
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.
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 (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".