Agda's emacs-mode is probably the most developed form of this available today, although Coq's tactics are doing roughly the same thing.
Types can't be wrong in the same way that values can be. Rather, to be more specific, in any circumstance where program derivation could even remotely succeed you will have had to have been specific enough with your types that they cannot easily produce the wrong code. It simply would fail to typecheck---at least eventually.
I wouldn't say that program derivation is limited to demo-level code, I would just say that you cannot expect proof search to achieve large fragments of code. It's just too large of a space!
Instead, it's better to think of it as an interactive game. You describe types as best as you can leaving holes where you haven't figured out what you want. The compiler responds telling you information and guesses about those holes. Furthermore, if you can nail down what you must prove sufficiently well to have confidence that it's the right thing then the compiler can probably do the trivial final details for you.
If you look through Conor McBride's (admittedly vast) literature then you'll find many things discussing this idea with respect to his (now defunct) experimental dependently typed language called Epigram.
I really like this analogy to interactive games, thanks!
I kind of see, logically, that the types can't be wrong in quite as many ways as the code/values/terms, but that's still a (possibly) infinite amount of wrong to contend with! Yes, we can, and frequently do, narrow it down, but still... :)
I've been aware of Mr. McBride's literature for some time, but I haven't ventured in beyond a cursory look at that ridiculously-well-punned Sinatra one. ("Do be do"... something?). It's a bit beyond what I can manage, in theory terms, at the moment.
EDIT: Sorry to sound like an excited puppy, but I don't think the time/place was quite right for me to have gone into or explored this field as I would have liked to as an undergraduate.
The thing about being wrong with types is that the end result is an immediate compiler failure. It can be difficult to figure out the right types, but once you do they're certain to behave properly. Thus, the penalty for wrongness is nearly nothing at all.
You face the infinite amount of wrong by working really hard to understand the right.
If you're wrong in values it'll probably still work for a while until it suddenly doesn't for rather mysterious reasons. This can be way down the line, undetected for a long time if not forever. Thus, the pain of being wrong is potentially infinite as well.
So, programming in types is no easier. It's probably even harder today since so few people do it. But the consequences are amazingly different.
And yeah, with Conor's work its "come for the puns, stay for the mind blowing computer science"
> the penalty for wrongness is nearly nothing at all.
Well, I think Edwin Brady showed a couple of C++-template-errmsg-like-things during a couple of his talks, but having actually programmed semi-advanced C++-template things I think I can agree on the general thrust that type-level problems are in some sense "better problems to have".
Btw, thanks for the exchange. (This is getting too off-topic, so I'll leave it at that.)
Types can't be wrong in the same way that values can be. Rather, to be more specific, in any circumstance where program derivation could even remotely succeed you will have had to have been specific enough with your types that they cannot easily produce the wrong code. It simply would fail to typecheck---at least eventually.
I wouldn't say that program derivation is limited to demo-level code, I would just say that you cannot expect proof search to achieve large fragments of code. It's just too large of a space!
Instead, it's better to think of it as an interactive game. You describe types as best as you can leaving holes where you haven't figured out what you want. The compiler responds telling you information and guesses about those holes. Furthermore, if you can nail down what you must prove sufficiently well to have confidence that it's the right thing then the compiler can probably do the trivial final details for you.
If you look through Conor McBride's (admittedly vast) literature then you'll find many things discussing this idea with respect to his (now defunct) experimental dependently typed language called Epigram.