12 Checks at the Boundary🔗ℹ

Examples with literal arguments can make checking look entirely static. In a real program, however, values arrive from outside the program, and we cannot know anything about them for certain. For instance, suppose we need the user to specify a payment amount. If they type it into a Web interface, the program cannot know what they entered; they may even have entered a negative “payment”.

Therefore, we cannot supply unknown values directly to functions with refinements. We instead need run-time checks to establish what the functions expect:

fun push({t :: Turnstile | !is_locked(t)}) :: Turnstile:

locked(0)

fun press(t :: Turnstile) :: Response:

if is_locked(t)

| refused()

| succeeded(push(t))

The good news is that if we leave out the test, or test the wrong thing, Liquid Shplait will report an error: e.g.,

Thus, refinements do not remove run-time checks from a program’s entry points. Rather, they ensure that each check exists, is in the right place, and is strong enough. All code past the entry points never needs to repeat the dynamic checks, and is checked entirely statically. The example "turnstile.rhm" is a complete program in this style.