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 :-)