Vary started out Python-shaped. The early syntax borrowed def, for...in, if/elif/else, import and from...import directly. If you had written Python, the first version of Vary looked familiar.
It diverged quickly. Static types are enforced at compile time. Blocks use braces. Mutation testing is a compiler command. The test runner is built into the language. Enums carry payloads. None of this exists in Python.
If terms like ghost code, proof obligations, invariants, or exhaustive match are unfamiliar, see the Glossary.
Python showed that code can be readable without being verbose. Short keywords, minimal ceremony, no semicolons.
| Area | Python | Vary |
|---|---|---|
| Typing | Dynamic, optional hints | Static, enforced at compile time |
| Execution | Interpreted | Compiled to JVM bytecode |
| Variables | x = 42 (always mutable) | let x = 42 / mut x = 0 |
| Null handling | Anything can be None | Only T? types can be None |
| Data types | @dataclass | data keyword |
| Enums | enum.Enum | enum with payloads and exhaustive match |
| Testing | pytest, unittest | Built-in test DSL + observe |
| Mutation testing | Third-party (mutmut) | Built-in vary mutate |
For a full comparison, see Python comparison.
Eiffel pioneered Design by Contract: preconditions, postconditions, and class invariants checked at runtime. Vary's contract system (in/out/old) draws directly from Eiffel's model.
| Area | Eiffel | Vary |
|---|---|---|
| Preconditions | require block | in {} |
| Postconditions | ensure block | out (result) {} |
| Entry-state capture | old expr | old(expr) |
| Class invariants | invariant block | invariant {} on classes and data types |
| Contract enforcement | Runtime, can be disabled per build | Runtime, always on in vary mutate |
| Mutation integration | None | Contract violations are mutation kill signals |
Eiffel treats contracts as documentation and correctness aids. Vary treats them as oracle surfaces for mutation testing. A contract that fails under mutation means the program is well-constrained. A contract that no mutation can break is too weak. Contracts in Vary exist to make vary mutate more powerful, not to prove formal correctness.
Two D ideas influence Vary: the pure function qualifier and built-in contract syntax.
| Area | D | Vary |
|---|---|---|
| Purity | pure qualifier, compiler-enforced | pure def, compiler-enforced |
| Contracts | in {} / out {} blocks on functions | in {} / out (result) {} |
| Contract scope | Preconditions, postconditions, invariants | Preconditions, postconditions, old(expr) |
| Mutation testing | None built in | Built-in vary mutate |
| Compilation target | Native machine code | JVM bytecode |
D enforces purity for safe parallelism and optimization. Vary enforces purity to improve mutation testing signal. A pure def guarantees no hidden state, so surviving mutants point to genuine gaps in contracts or tests rather than side-effect interference. D proved that purity enforcement is practical in a mainstream-style language. Vary applies it to a different problem.
Dafny is a verification-aware language. Programs are proved correct at compile time using an SMT solver (Boogie/Z3). Contracts written in Dafny are not runtime checks: they are static proof obligations that must hold before the compiler will emit code.
| Area | Dafny | Vary |
|---|---|---|
| Verification | Static proof via SMT solver (Boogie/Z3) | Runtime contracts + mutation testing |
| Preconditions | requires | in {} |
| Postconditions | ensures | out (result) {} |
| Pre-state capture | old(expr) | old(expr) |
| Invariants | invariant on classes and loops | invariant {} on classes and data types |
| Termination | decreases clause (compiler-checked) | Not enforced |
| Frame control | reads / modifies clauses | No frame specifications |
| Ghost code | Ghost variables and functions (erased at compile time) | No ghost constructs |
| Null handling | T? for nullable types | T? for nullable types |
| Variables | var (mutable) / const (immutable) | mut (mutable) / let (immutable) |
| Compilation targets | C#, Java, JavaScript, Go, C++ | JVM bytecode |
| Mutation testing | None built in | Built-in vary mutate |
| Testing | Specifications replace most tests | Built-in test DSL + observe |
Dafny proves that a function is correct for all inputs. Vary does not attempt formal proofs. Instead it checks contracts at runtime and uses mutation testing to measure how well those contracts and tests constrain behaviour. A surviving mutant in Vary means a gap exists. An unproved postcondition in Dafny means the solver cannot confirm correctness.
The two approaches fail differently. Dafny proofs can require heavy annotation (decreases clauses, loop invariants, lemma functions) to satisfy the solver. Vary contracts are lighter to write but weaker: they catch violations only when exercised by tests or mutants, not for all possible inputs. Dafny targets provable correctness. Vary targets confidence through fault injection.