Pleased to announce a new language, liquid-typed shplait. shplait is Matthew Flatt's typed (t) shrubbery-syntaxed (sh) language for the book PLAI (plai).
This version adds liquid typing, and some restrictions to make that work. Liquid typing is a form of refinement-types. Basically types carry along refinements that are automatically discharged by a solver (specifically, Z3).
Liquid Shplait is not really meant to be a production language, though of course if someone wants to use it inside production code, go ahead! One of its current restrictions is that it does NOT check refinements at module boundaries. That means you won't get contract wrappers that check whether you're violating the liquid types. The advantage is that it doesn't impose any runtime overhead either, which can be quite a bit for some of those refinements.
You can, for instance, take some tricky numeric or other subsegment of your code and move it into the Liquid Shplait language, have much richer type-checking in there, feel confident that you got things right (e.g., bounds checks), and then export the functions and use them from regular Rhombus or Racket code.
Liquid Shplait is here:
For some examples, see here: