Exfer Script: Always-Halting Scripts
The conditions under which a coin on Exfer can be spent are expressed in a language called Exfer Script. The language guarantees, by construction, that every script terminates and that every script's execution cost can be computed exactly before it runs.
This is the sharpest design divergence between Exfer and Ethereum.
The cost of Turing-completeness
Ethereum's EVM is Turing-complete — in principle it can express any program. The price is that you cannot statically decide how long a contract will run (the halting problem is undecidable). So the EVM uses gas as a backstop: every step costs gas, run out of gas and execution halts. This keeps the network from hanging forever, but leaves a long list of side effects:
- Complex contracts' execution cost can only be estimated, not computed — hence the entire gas-estimation machinery
- Reentrancy attacks: contract A calls contract B, B calls back into A, and state becomes inconsistent — the 2016 DAO hack drained ~$60M from an Ethereum smart contract this way
- State dependence: the same transaction may produce different results at different block heights
- Formal proofs are nearly impossible: you cannot rigorously prove an EVM contract is correct
Human developers can work around these. Autonomous programs cannot tolerate "the code might hang" or "the result might vary."
Exfer's alternative: total functional combinators
Exfer Script is not Turing-complete. It belongs to a class called total functional combinator languages:
- total = defined output for every input; no undefined behavior
- functional = no side effects, pure functions
- combinator = built from finitely many basic combinators; no
while, no general recursion
Exfer Script is a bounded-depth expression tree. The language itself prevents you from writing infinite loops — there is no while(true), no arbitrary recursion.
What this buys you
| Property | EVM | Exfer Script |
|---|---|---|
| Guaranteed to halt | No (relies on gas) | Yes (by syntax) |
| Execution cost known in advance | Estimated | Exactly computable |
| Reentrancy attacks | Real, historically exploited | Impossible by model |
| Global mutable state | Yes; a source of bugs | None; state is local |
| Formal verification | Difficult | Practical |
What this design can and can't do
Can do: all the core payment-layer patterns — multisig, timeout refunds, escrow, delayed unlocks, delegated authority, atomic swaps. Each is a built-in CLI command (see Built-in script templates).
Cannot do:
- Uniswap-style AMMs: require arbitrary loops and unbounded state access
- Decentralized lending (Aave/Compound): depends on composable Turing-complete contracts
- Complex derivatives / perpetuals: same
- On-chain NFT auctions with arbitrary logic: simple ones yes, complex auction mechanisms no
Exfer assumes M2M payments and DeFi have different requirements. Paying between machines, escrow, dispute resolution — these do not require Turing-completeness. What they require is absolute predictability. The tradeoff is deliberate, not a ceiling.
Historical context
Non-Turing-complete scripting languages predate Exfer. Blockstream's Simplicity project — a research effort to give Bitcoin a provably-correct contract language — has been on this path for years. Exfer Script sits in the same lineage.
Further reading
- Built-in script templates: HTLC / Multisig / Vault / Escrow / Delegation — how the five common patterns are used
- The UTXO data model — why "state is local" comes for free under UTXO
- Glossary / Exfer Script — one-line definition
- Protocol specification — complete script language reference