[HN Gopher] Program Synthesis is Possible (2018)
___________________________________________________________________
Program Synthesis is Possible (2018)
Author : xept
Score : 87 points
Date : 2022-09-04 10:27 UTC (12 hours ago)
(HTM) web link (www.cs.cornell.edu)
(TXT) w3m dump (www.cs.cornell.edu)
| lapinot wrote:
| 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".
| bjourne wrote:
| > 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 wrote:
| Fftw?
| _0ffh wrote:
| "Fastest Fourier Transform in The West" http://fftw.org/
| lapinot wrote:
| 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=Per
| l&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 wrote:
| 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.
| DavidRogers0000 wrote:
| turnsout wrote:
| 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.
| vivegi wrote:
| 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.
| mirker wrote:
| Imagine building a compiler optimization pass. Do you want to
| hand-roll all the shifting equivalence relationships for
| division, etc?
| sanxiyn wrote:
| 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....
| LanternLight83 wrote:
| 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
| _0ffh wrote:
| 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.
| jongjong wrote:
| 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.
___________________________________________________________________
(page generated 2022-09-04 23:01 UTC)