Why replace Racket with Pyret? Is this purely to stop students from being able to complain about syntax or is there a deeper strategic reason behind this?
Refinement types are nice. I really wish those were more common.
Your second paragraph answered your first paragraph (-:.
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!)
I am also convinced that parenthetical syntax has real problems that I can't completely ignore.
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?
Refinement types are nice. I really wish those were more common.