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 (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".

> 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.

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.