Love this. I’ve been working on and off on an inductive programming library for JavaScript. In my head the mental model I have is to treat expressions as similar building blocks with strongly typed inputs and outputs that the solver wires up together to construct programs. I’ve thought about creating a visual debugger to show this - similar to what’s described here - to make it easy to visualize and understand what the library does.
I suppose this points to the relationship between proving and programming.
With proofs, I get the impression that much of the ingenuity comes from being able to pull in really useful building blocks, and wiring things up is maybe a secondary (more fundamental) skill. Maybe the programming parallel to that is pulling in a great library vs gluing code together.
Love this. I’ve been working on and off on an inductive programming library for JavaScript. In my head the mental model I have is to treat expressions as similar building blocks with strongly typed inputs and outputs that the solver wires up together to construct programs. I’ve thought about creating a visual debugger to show this - similar to what’s described here - to make it easy to visualize and understand what the library does.
I suppose this points to the relationship between proving and programming.
With proofs, I get the impression that much of the ingenuity comes from being able to pull in really useful building blocks, and wiring things up is maybe a secondary (more fundamental) skill. Maybe the programming parallel to that is pulling in a great library vs gluing code together.
The post and the links to other such efforts reminded me of the graphical interface used by the scientists in “The Zero Theorem”