I hope the next languages will come from interactive theorem provers and program synthesis. I'd much rather work at the level of types, propositions, models, an

I hope the next languages will come from interactive theorem provers and program synthesis. I'd much rather work at the level of types, propositions, models, and proofs and solve the interesting problems. The rest is book keeping and often repeated over and over. And I hope the interfaces for these languages won't require the use of a glowing screen and a sadistic keyboard. I'd rather like it for computers to disappear into the background. I'd like to reason about my programs in a physical space where I can freely walk around, write on a note pad, draw on a chalk board, converse, and re-arrange the room to my liking. I quite dislike how I've developed astigmatism, am at high risk for RSI, and probably other health ailments because we can't think of a computing environment better than what we have right now... just with more pixels, pop ups, nags, swishy animations, etc.