Liquid Shplait🔗ℹ

Liquid Shplait implements “liquid” typing. Liquid types are a long line of work by Ranjit Jhala and collaborators, starting with this one. Liquid types are a form of refinement types, which were originally added to modern programming languages in this work. Here’s a more recent survey on the concept of refinement types. Liquid Shplait is directly inspired by and based on these ideas.

While the program compiles, the checker turns every such claim into proof obligations and asks the Z3 solver to discharge them. If the body were n / 2 or n - 2, the program would not compile:

Checking refinements happens purely statically. The checker does not add run-time checks: any refinement that cannot be checked is rejected, not turned into a run-time check. Checking happens as part of type-checking, so if the program compiles (e.g., in DrRacket you see the REPL prompt), that means all the checks have passed.