Lambda the Ultimate

Frankly, I'm just happy others see this as an interesting avenue of research, even if the road is long long to getting to something that works. I've been thinking a lot about this lately. Programming as a problem solving activity basically abstracts concrete examples (usually with paper and a white board, our existing programming environments do not help much). 2D graphical domains have the most obvious path to supporting this process using a programming environment, and it shouldn't be a surprise that we start there.

So the first step is to figure what we are doing for 2D graphics, then the next step is to break out of the 2D box. Even in the first step, there is a lot to do; how do we create parametric 2D diagrams via direct manipulation?

And the last paragraph of my post above sounded pretty harsh and pompous when I re-read it, so I edited it and toned it down. I didn't change the point I was trying to make, which is basically that, if you generalize enough, the problem becomes "programming by example" (provide inputs and outputs and the compiler will generate the program) which is AI complete / very hard. I would rather focus on making it easy to build user specified manipulable visualizations rather than trying to automate too much.

Yes it does! On the other hand, programming by example can be made more feasible by making it more interactive: the compiler just doesn't choose an implementation, but helps you find one based on known inputs and outputs. Direct manipulation is just w way to express concrete inputs and outputs...we are then just missing the faculties to abstract between the two (like add a unifying variable when two properties have similar values).

Given a specification for a program as a type (dependent type, or logic meta-program), an implementation of that specification is a proof. Programming by example becomes a proof search, and what you are looking for is a guided proof search. I am interested in this, but from a REPL sort of interface. Of course like python workbooks, the program input and output could be graphics or graphs.

Most programs don't involve proofs, so this approach doesn't appeal to me, but isn't that exactly what COQ does already?

Badly. Does badly.

Most programs do not include proofs they are the proof. For example I want a program with the type signature : forall a . a -> a, does such a program exist? What is the shortest proof? The proof is the implementation, and in this case it is trivial to find (\x . x). Yes Coq can do this, and that was my point, the technology to do what you want already exists. I prefer Twelf.

A set of examples doesn't constitute a very rigorous specification, though. Programming-by-example is usually severely under-constrained.

Degenerate is fine, as you stop on the first solution, or find the shortest solution (within bounded time or search depth). For a simple example consider the type:
forall a b . (a, c, b) -> (a, d, b) which is underspecified (we effectively don't care what c and d are). It's fairly easy to see how this can be extended to arbitrary arrays of numbers with unknowns representing input and output vectors (you only need a type level encoding for ints. So a function to map the array [1, ?, 3] to [2, ?, 4] becomes the search for a function to implement the type: ((()), a, (((())))) -> (((())), b, ((((()))))), or something like that with a better encoding of ints. The shortest solution is (\x . x + 1), of course by pure search this might be difficult to find, you might need t give a strategy hint to try applying the same transform to all elements, and then search a library of simple arithmetic operators to see if any fit (or nearly fit).

I find that there is a large over-interpretation of the Curry-Howard correspondence, and I would recommend avoiding the claim that "programs are proof". In my experience, this point is often misunderstood and leads to claims that are blown out of proportion. On the contrary, claiming that "proofs are programs" seems to have a much lower nuisance potential.

I do more than agree on the general point that techniques derived or inspired from proof search can be helpful to program synthesis. (I have not yet read the paper cited in this thread, but I'm not sure it is so relevant in this case.) The idea that examples can be understood as a form of under-specification, and integrated in a more general proof-search-inspired synthesis mechanism, has been realized in particular in Example-Directed Synthesis: A Type-Theoretic Interpretation, by Jonathan Frankle, Peter-Michael Osera, David Walker, and Steve Zdancewic, 2016, which you may be interested in.

I think your point is that most programs don't prove anything useful. For example a lot of programs prove the Haskell type IO () is inhabited, yet they all do different things. This argument is somewhat weakened by Haskell having no side effect control. What happens when the hypothesis includes more meta-information about the program than just types, but can include static values, and other properties. This is why I tend to view a hypothesis as a meta-program and not a type, so its no longer limited by curry-howard.

Haskell programs only prove things in a very boring logic; specifically the logic where all propositions are provable. This is one of the reasons that gasche's claim is right -- very few typed programs "prove" anything in a logic of any interest.

This is not only the same elephant as programming-by-example, but also the same elephant as aspect-oriented programming. In all of these, the problem is how to deduce the whole from some parts (which is of course, meta, the problem with the elephant as well).

Well, if you "parameterize" the sliders instead then you get the kind of visual programming you see in 3d content tools. That seems to have won out versus regenerating textual code as in this svg example.

I want to have it and consume it. I want the sliders and the ascii. I want it all working together. I don't want to have to choose one or the other.

Well, with Maya you have Maya Ascii - but I doubt you'll really want to look at it.