Refinement types are nice. I really wish those were more common.
1. We have a different view of static typing than Racket.
2. We have a different view of the type language than Racket.
3. Long term, we are working on smoothly integrating testing, types, and specification [as a spectrum -- perhaps even as a cycle -- rather than as three different things]. Refinements are an instance of this. Another is our plan for how to do type inference.
4. I am also convinced that parenthetical syntax has real problems that I can't completely ignore. Of course, it doesn't hurt if it can get people to stop complaining. (It's not only students: the bigger opposition often comes from teachers. Unfortunately the teachers control the path to the students, so their views _really_ matter!)
What brought you to this conclusion? Experience from Bootstrap (in which I found arithmetic and parenthesis counting to be the biggest stumbling blocks) or just personal reflection?
Our goal is to eventually create language levels, pioneered by DrRacket, based on what we learn from observation. This is a research project in addition to a development one, where the research is into human factors.