What removal looks like

Removing the gap means having one artifact. The rule a human writes must be, literally and byte for byte, the thing the chain enforces. That requires the chain to enforce logic directly: no compilation into an executable form the author never reads, no machine whose behaviour stands in for the author's meaning. A transition is admitted when the stated conditions are proved to hold over it, and refused otherwise.

That is what Modulus is. The next two pages describe the mechanism: what a predicate is and why it occupies the slot a contract occupies, and how proofs admit state transitions.