Open Standard · Working Draft
mekaniskt·kontrakt

Specification ·  Section 9 of 13

Why if + which is enough

The rule language is deliberately starved to conditions, exhaustive pattern matches, bounded arithmetic, and effects, which buys decidability, readability, and immunity to whole classes of smart-contract exploits.

The rule language is deliberately starved: conditions (if), exhaustive pattern matches (which ... is ... otherwise), arithmetic with declared rounding, and effects (reserve/draw/record/accept/reject/notify). The only iteration is the implicit bounded map over payload lines. That starvation buys:

  • Decidable everything. Termination is structural (no loops), exhaustiveness is checkable (which must cover or have otherwise), pool safety (“no event sequence drives a pool negative / past capacity”) is verifiable because state changes only through declared effects. The full property-test battery runs on every save.
  • Readable by the people who sign. An upphandlare reads which line.item is hours.senior: expected := rates.senior at line.period aloud and it is the contract clause. This is Catala’s literate lesson applied at the syntax level.
  • Nothing to exploit. No reentrancy, no gas games, no overflow (decimals with declared rounding, bounds-checked pools). The Solidity exploit genre dies of starvation - most smart-contract CVEs are expressiveness the mechanical contract simply does not have.

Expressiveness grows only by adding vetted primitives when the corpus demands them (a rental.claim port with deposit/return semantics the day a hyresavtal needs it; a material.delivery port with despatch-advice payloads for goods frameworks) - never by adding computation.