This is about language design.
From a post in the Lambda the Ultimate Blog ( http://lambda-the-ultimate.org/node/5350 ) I’ve found two papers about the experimental implementation of refinement types in Typed Racket and TypeScript (that are a statically typed Scheme and Java Script):
“available on-line, free to all until 2 weeks after the conference”, from this page:
“Refinement types for TypeScript”, by Panagiotis Vekris, Benjamin Cosman, Ranjit Jhala (PDF file):
Try it online:
“Occurrence typing modulo theories” by Andrew M. Kent, David Kempe, Sam Tobin-Hochstadt (PDF file):
The article about TypeScript is the most interesting of the two. Rust cares a lot about code correctness, and it’s already very-strongly and very-statically typed, so to me it seems a good language to introduce refinement types, despite their current limits.