4 ms·

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

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.
  - lapinot 4y ago
    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.

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.
- lapinot 4y ago
  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.