Design by contract: require / ensure / assert

require checks a precondition, ensure a postcondition, and assert is the same primitive used standalone โ€” all three lower to one contract_check host call, enforced identically whether interpreted, run here via WASM (no rustc at all), or compiled natively. The last line deliberately violates a precondition so you can see enforcement fire.

PatLang source
# Design-by-contract demo in the Stage 1 self-hosted language.
# `require` checks a precondition, `ensure` a postcondition (checked wherever
# it's written โ€” usually right before the value it names is returned), and
# `assert` is the same primitive used standalone. All three lower to the
# same contract_check(func, kind, text, ok) host call, so enforcement is
# identical whether interpreted, run via run_ir (no rustc), or compiled
# natively. The last line deliberately violates a precondition, to show
# what enforcement actually looks like.

make a function called safe_divide takes a, b returns r
  require b != 0
  let r = a / b
  ensure (r * b) == a
  return r
end

make a function called clamp takes x, lo, hi returns r
  require lo <= hi
  if x < lo then
    let r = lo
  else
    if x > hi then
      let r = hi
    else
      let r = x
    end
  end
  ensure (r >= lo) and (r <= hi)
  return r
end

make a function called factorial takes n returns r
  require n >= 0
  if n < 2 then
    let r = 1
  else
    let r = n * factorial(n - 1)
  end
  ensure r >= 1
  return r
end

print("safe_divide(10, 2) = " + safe_divide(10, 2))
print("clamp(15, 0, 10) = " + clamp(15, 0, 10))
print("clamp(-5, 0, 10) = " + clamp(-5, 0, 10))
print("factorial(6) = " + factorial(6))

assert (1 + 1) == 2
print("standalone assert passed")

print("--- now deliberately violating a precondition ---")
print("safe_divide(1, 0) = " + safe_divide(1, 0))
print("(unreachable: the line above aborts the program)")

(not run yet)

Native run on the build machine:

safe_divide(10, 2) = 5
clamp(15, 0, 10) = 10
clamp(-5, 0, 10) = 0
factorial(6) = 720
standalone assert passed
--- now deliberately violating a precondition ---
IR runtime error: contract violation: precondition failed in safe_divide(): (Var(b) != Num(0))