Sources of inspiration and interesting directions for programming languages
plsadventures.blogspot.com
plsadventures.blogspot.com
Exotic type systems: he advocates dependent types. There appears to be an error is his second example (I dont know ML), so I cant quite follow he=is example. OTOH I implemented a program generation system a decade ago which included type composition and type reasoning, so I think we agree that there is much more interesting stuff that can be brought to mainstream languages.
He advocates strong static typing with type inference. I like Python 3's approach: duck typing with optional type declarations, although in Python 3 they are in effect just comments.
Visual programming languages. he thinks it's a good idea, but hasnt seen any good examples. I would go so far as to say all the ones I have seen are bad. I would welcome some good visualization tools for existing languages.
Concurrent programming languages: he mentions Occam and several others. He thinks Bigraphical Programming Language has promise.
Theorem proving: he is looking for something less ambitious than proving program correctness, maybe more along the lines of eclipse's error helpers. He suggests tools that ask your intent. I too would welcome tools that can reason about programs, that can attempt to understand the programmers intent and can answer questions about the systems implementation.
MindRover was one example. It's a robot programming game I was involved with, released in 1999. You would put components such as radars and weapons on your vehicle. When you went to program the vehicle, it would show you the components you selected, and you could draw wires between them. The wires would create events of the form "when the radar sees the enemy, fire the laser".
You could develop fairly complex behaviors. For example, there was a logical component which worked like a state machine: you could say "when the nearby radar sees the enemy, enter the run-away mode", and program the run-away mode to ignore the radars and drive in random directions. There were also 'variable' components that kept state and could remember values from one event to the next. I am pretty sure it was Turing-complete, although sort of awkwardly so. (The events were compiled into an object-oriented language which just defined methods for everything)
MindRover's execution model was sequential in response to events, but I think this sort of event-driven visual programming would work well as a concurrent system, because it makes it hard to depend on the internal state of other components.
I guess the interesting question is whether we can even begin to approach generality.