MEP 7. Soundness

Field	Value
MEP	7
Title	Soundness
Author	Mochi core
Status	Active
Type	Process
Created	2026-05-08

Abstract

A type system is sound when "well typed programs do not go wrong." This MEP states what we mean by sound for Mochi, lists the property-by-property test obligations that we use to verify soundness, and records the escape hatches we accept today. It is a process MEP because it is the contract that future feature work has to satisfy.

Motivation

Mochi has both an interpreter and a bytecode VM. Without a written contract, neither backend has a clear standard against which to ship a feature. The Wright and Felleisen formulation gives us two clean lemmas: progress and preservation. Reducing soundness to those two statements lets us write fixtures that mechanically verify the contract.

Specification

What we mean by sound

The standard Wright and Felleisen formulation is two lemmas plus a corollary.

• Progress. If ∅ ⊢ e : τ then either e is a value, or there exists e' such that e ↦ e'.
• Preservation. If Γ ⊢ e : τ and e ↦ e' then Γ ⊢ e' : τ.
• Type safety. By induction, no well-typed term reduces to a stuck configuration that is not a value.

Mochi has both an interpreter and a bytecode VM. Soundness in the language statement above is against the interpreter's reduction relation. The bytecode VM should agree with the interpreter on all typed inputs but it lags on agent and logic features and is therefore treated as a separate target with its own conformance suite.

Mochi-specific values

Values in this language at v0.10.82:

• Integer literals at the four widths.
• Floats.
• Booleans.
• Strings.
• Null.
• Lists of values.
• Maps of values.
• Closures, both block-bodied and arrow-bodied.
• Struct instances and union variant instances.

Stuck states we want to rule out:

• Calling a non-function.
• Indexing a non-list and non-map and non-string.
• Iterating over a non-iterable.
• Comparing values of incompatible types.
• Adding a string to an integer.
• Pattern matching against a value with no matching arm and no wildcard.
• Reading a non-existent struct field.
• Dividing an integer by zero. The runtime raises today; the type system does not flag the literal case.
• Reading a missing map key without a default. Today the runtime returns the zero value of the map's value type, which violates progress for non-zero-bearing types. Tracked in MEP 4.

Property-by-property obligations

The properties below are the test obligations against which fixtures are built. Each property points at the MEP where the rules live and at the fixture group in tests/types/. The full coverage matrix lives in MEP 9; the table here is the inline summary for reviewers who want to confirm a property has at least one fixture without leaving this MEP.

Property	Source MEP	Fixture pointer
Progress, primitives	MEP 4	tests/types/valid/canonical_*
Progress, list/map	MEP 4	tests/types/valid/list_*, tests/types/valid/map_*
Progress, function	MEP 4	tests/types/valid/closure_*
Preservation	MEP 5	tests/types/valid/preservation_let_chain.mochi
Inversion	MEP 5	tests/types/valid/inversion_*
Canonical, bool	MEP 4	tests/types/valid/canonical_bool_only.mochi
Canonical, int	MEP 4	tests/types/valid/canonical_int_arithmetic.mochi
Canonical, string	MEP 4	tests/types/valid/canonical_string_concat.mochi
Substitution	MEP 5	tests/types/valid/preservation_let_chain.mochi
Variance	MEP 11	none yet, tracked in MEP 11
Parametricity	MEP 12	none yet, tracked in MEP 12
Exhaustiveness	MEP 13	tests/types/valid/match_union_variant.mochi
Alpha equivalence	MEP 8	none yet, awaiting property-test layer

Progress

If a closed expression has type τ, evaluating it never gets stuck on a missing rule. Tests:

• For every primitive, evaluate a literal of that type.
• For every binary operator at every level, evaluate a closed expression at the level boundary.
• For every postfix operator (call, index, field, cast), build a closed expression and evaluate it.

Preservation

If e ↦ e' we re-type e' and check the type matches. We do not have a step-level reduction relation in the runtime, so we approximate by:

• Inserting let bindings around sub-expressions and asserting the outer program still type checks.
• Replacing reducible sub-expressions with their values and asserting the outer program still type checks.
• For function calls, asserting the call site type equals the inferred type of the call's substituted body.

Canonical forms

For every type, fixtures assert:

• The set of values at that type.
• A negative fixture rejects a value not at the type.

For example, at bool, the only values are true and false. A fixture asserts that 1 + 2 == 3 evaluates to true of type bool. Another fixture asserts that print at type void cannot be assigned to a variable.

Inversion

For each typing judgement form we have one fixture per shape. The shape mappings are listed in MEP 5.

Substitution

For every binding form, a fixture asserts that replacing the binder with its value preserves the type and the result.

let x = e1 in e2     ≡   e2[x:=e1]   when e1 has no side effects

For mutable bindings, we test sequencing instead.

Variance

Fixtures cover the following positions:

• Function argument and result, asserting the contravariance of the argument and the covariance of the result.
• List element, asserting the current behaviour: covariant when read, unsafe when written. The unsafe case is a known weakness in MEP 10.
• Map key and value, asserting invariance.

Parametricity

For each generic builtin (len, first, reverse, distinct, push, keys, values, range), fixtures assert:

• The result type tracks the input element type when known.
• Two distinct call sites do not leak through the type variable.

Once parametric polymorphism is wired through, we add the standard parametricity tests: a polymorphic function applied to a list of int and a list of string must commute with map.

Exhaustiveness and irredundancy

For each tagged union declaration in fixtures:

• A match covering every variant type checks.
• A match missing a variant fails today (when implemented; flagged in MEP 13 as a hole).
• A match with an arm that is a strict subset of an earlier arm fails (when implemented).

Alpha equivalence

For every binding form, two fixtures with bound names renamed must produce the same goldens after the rename. We do not author both versions by hand: we automate alpha rename in a property test.

What we accept as not sound today

The escape hatches we acknowledge. Each row points at the MEP that owns the fix and at the fixture pinning current behaviour, when one exists.

Escape hatch	Tracked in	Pinning fixture
AnyType unifies in both directions	MEP 11	none yet, planned any_top_silent_widen
as cast accepted without compatibility check	MEP 11	none yet, planned cast_int_as_string
null is any rather than an option type	MEP 4, MEP 10	none yet
Aliasing a let aggregate into a var allows a write through the alias to mutate the original	MEP 15	tests/types/valid/mutate_through_let_alias.mochi
Reading a missing map key returns the zero value	MEP 4	tests/types/valid/missing_map_key.mochi
Integer division by zero is a runtime panic, not a checker rejection	MEP 5	none yet

Listing the fixture column on the right is uncomfortable on purpose. Every blank cell is a bug we have decided not to flag yet; the decision should be deliberate.

Conformance between interpreter and bytecode VM

A program that the type checker accepts and the interpreter executes should produce the same observable output when executed by the bytecode VM, with the documented exceptions below. Last audited 2026-05-08 against v0.10.82.

VM gap	Reason	Status at v0.10.82
intent method calls	Reactive runtime not on VM	Calling an intent crashes the VM with stack overflow.
on event handler dispatch	Reactive runtime not on VM	Declaration accepted; handler does not fire on emit.
emit statement dispatch	Reactive runtime not on VM	Statement runs; no handler is invoked.
query against logic facts	Logic engine not on VM	Execution hangs; dataset queries are unaffected.

agent, stream, fact, and rule declarations are accepted by the bytecode VM today. The gaps are in runtime dispatch and in the logic engine, not in the parser. query over dataset sources continues to work on the VM and is not on this list. The conformance test set lives at tests/vm/ and runs the same source through both backends, asserting equal stdout. The audit method is to write a small probe per row (agent declaration, on/emit pair, intent call, fact/rule declaration, query over logic facts) and run it through mochi run, recording whether the program finishes with the expected output. This list should be re-audited every release; if a feature has been wired through to bytecode, drop the row and update the audit date.

Rationale

Wright-Felleisen is the standard formulation for ML-like languages. We adopt it because it gives us a property-by-property test plan that matches the way we already write fixtures.

We acknowledge the escape hatches in writing because pretending they do not exist is the fastest way to ship an unsound feature. Pinning current behaviour in fixtures makes a future tightening a deliberate breaking change rather than an accidental drift.

Backwards Compatibility

The escape hatches above will be tightened over time. Each tightening is a breaking change and will land with its own MEP and fixture migration plan.

Reference Implementation

• types/check.go — checker.
• types/infer.go — inference.
• tests/types/valid/ and tests/types/errors/ — fixture sets.
• tests/vm/ — interpreter versus bytecode conformance.

Open Questions

• Step-level reduction relation. We approximate preservation today. A formal small-step semantics would let us mechanise the proof. Out of scope for v0.11.0.
• Property test infrastructure. Alpha equivalence and other meta properties want a generator-based test framework. Track in MEP 8.

References

• Andrew Wright and Matthias Felleisen, "A Syntactic Approach to Type Soundness", Information and Computation, 1994.
• Benjamin C. Pierce, Types and Programming Languages, MIT Press, 2002.

Copyright

This document is placed in the public domain.