4 ms·

> The main problem with that idea is that you have to find some language to describe the design, which often ends up being an implementation, and when you look

> The main problem with that idea is that you have to find some language to describe the design, which often ends up being an implementation, and when you look at the invariants that must be maintained for correctness, it's difficult to deviate from that implementation substantially. Can we please stop repeating this line? It was false 50-60 years ago when garbage collection and register allocation was invented. It was false when yacc was built. And it's false today. The gap in detail between specification and implementation is huge. If you can change a function without changing its callers, then your program has some slack between the assumptions placed on that function and its implementation. From low-level performance things like changes to improve cache locality, to high-level ones like scheduling of data pipelines, there's a lot of space for synthesizers and search-based software improvement tools to work with. So, are you curious about program synthesis for floating-point accuracy? Have a look at Herbie.

jcranmer 8y ago
> Can we please stop repeating this line? It was false 50-60 years ago when garbage collection and register allocation was invented. It was false when yacc was built. And it's false today. No, it's still very true today. We have pushed the bounds of what implementation details we are free to ignore, but those bounds are still very much on the order of "you have to program the algorithm I implemented" as opposed to "you have the freedom to choose any algorithm so long as the output obeys these mathematical constraints." Program synthesis techniques have improved and are improving, but they're still only really applicable to kernel-style transformations.
- Darmani 8y ago
  What's a kernel-style transformation? That term is unfamiliar to me? Are you referring to e.g.: optimizing stencil kernels? You're correct that classical semantics-preserving compiler optimizations are very restricted, when not user guided as in the OP's tool. They do not have any form of specification weaker than the input code. This is why most synthesis tools do take something higher level than code. Then again, some really do have the workflow "figure out existing code's algorithm, and pick a better one." The first thing in this space that comes to mind is verified lifting, being pursued by my collaborators at UW.

jcranmer 8y ago

> Can we please stop repeating this line? It was false 50-60 years ago when garbage collection and register allocation was invented. It was false when yacc was built. And it's false today. No, it's still very true today. We have pushed the bounds of what implementation details we are free to ignore, but those bounds are still very much on the order of "you have to program the algorithm I implemented" as opposed to "you have the freedom to choose any algorithm so long as the output obeys these mathematical constraints." Program synthesis techniques have improved and are improving, but they're still only really applicable to kernel-style transformations.

Darmani 8y ago
What's a kernel-style transformation? That term is unfamiliar to me? Are you referring to e.g.: optimizing stencil kernels? You're correct that classical semantics-preserving compiler optimizations are very restricted, when not user guided as in the OP's tool. They do not have any form of specification weaker than the input code. This is why most synthesis tools do take something higher level than code. Then again, some really do have the workflow "figure out existing code's algorithm, and pick a better one." The first thing in this space that comes to mind is verified lifting, being pursued by my collaborators at UW.