Lambda the Ultimate

IIRC, the Alfa interface for Agda 1 used the type system to guide structural editing, which is what you suggest here.

Alfa also included support for natural language editing, using Grammatical Framework. This natural language feature could use the type system for disambiguation. For instance, the input "for all numbers x, x is even or x is odd" would be disambiguated to "∀ x: nat. (even x ∨ odd x)", rejecting the ill-typed parse "(∀ x: nat. even x) ∨ odd x".

I've thought about this topic, but not yet read anything at all (so I'm pleased to learn the standard term for it). However, when I've thought a little deeper about the issue, I've tended to the view that the real productivity gains would come from something that has semantics in the generative structure. So I'm wondering if you have read anything along those lines.

The real value of free-form entry over syntax-directed entry is that when modifying exist code, the easiest path between two syntactically correct states may require going through syntactically incorrect states. Your hyptothetical editor will need to take this into account, allowing automation of as many common transformations as possible.

18 months ago, Thomas Lord argues for use of gestures in programming.

3 months ago, Sean McDirmid asks about programming with touch, noting Conal Elliott's tangible programming and Scratch.

Johnathon Edwards has been working on this problem via Subtext and UI programming languages. He posits that syntax must die and has done some interesting work on what he calls 'schematic tables' for resolving the expression problem in a visual language.

Edwards references work on gradual typing as of possible interest to visual language design. Gradual typing has been discussed several times on LtU [1][2][3].

I at one point was pursuing using types to direct a parse, similar as mentioned by vrijz above. I eventually decided against this because the very notion of bootstrapping an extensible syntax that is type-sensitive was tying my mind in knots, which seemed to violate simplicity goals.

Today, I would favor use of pluggable types and zero-button testing, integrating with the IDE and visual cues to let developers know about type-errors and broken tests just as easily as syntax highlighting helps developers discover syntax-errors today.

So I focus on language features that would help achieve continuous testing and analysis while we edit and (if we wish it) even during runtime: Object capability language makes it easy to confine unit tests and even many integration tests. Reactive languages allows tests to exist as 'continuous' programs during the whole edit cycle and even during runtime, though I feel we really need to capture most conditional branching and conditional binding within the reactive expressions (unlike Bling).

It seems to me the great challenge with this goal would be that it is quite difficult to limit expressions based upon types. For example, take the simple conditional expression: if _ then _ else _ :: Bool -> a -> a -> a.

This expression could be 'meaningful' in any context, since its output type is a function of its body. To ensure safety-by-construction will require ensuring that both the 'then' branch and 'else' branch produce a type compatible with both the context and one another (which raises a related challenge: how do you ensure the types on both branches are compatible continuously during edit, without overly hindering productivity?)

In the more expressive programming languages, this sort of 'option' seems to be very common - almost every aspect of glue-code has some sort of generic type. How many 'options' can be presented to the user before searching and selecting among them becomes less productive than writing out a little code and correcting for the occasional safety error?