Example of extended static checking
Displaying strings that fit on the screen
Fits ∈ Word32 → String → Prop puts ∈ (x,y∈Word32) → (s∈String) → Fits x s → InRange yRange y → H ()
Useful for the correctness of the "Hello world" program :-)