This language is cyuuuute! The multi-valuedness making "if (x | y) then…" work is so neat, and having `x : int` be a thing of exactly the same nature as `x = 3` is cool to see; even in a fully dependently-typed language, those things are not of the same kind. This looks super mind-expanding to try out!

(My first reaction is some slight aversion to what the "flexible" and "rigid" stuff is doing in the conditional scrutinee body, but maybe that'll feel natural after playing with the formal specification a bit.)