## What is property testing?

When you write a normal test, you pick specific examples: "if I pass 2 and 3, I should get 5." That works, but it only checks the cases you thought of. Property testing flips this around. Instead of choosing inputs by hand, the computer generates hundreds of random inputs and checks that a general rule holds for all of them. If the rule breaks, it tells you which input caused the failure.

[Hypothesis](https://hypothesis.readthedocs.io/) is the most widely used property testing tool for Python. Vary has a built-in equivalent called [`across`](/docs/test-dsl/#property-based-testing-with-across). This page compares the two.

## Vary vs Hypothesis

Both solve the same problem: example tests only cover cases the author thought to write down, while property testing generates many inputs against a general claim. Hypothesis does this as a Python library (the `given(...)` decorator with strategies). Vary does it inside the language (`across(...) { observe ... }` with typed bindings).

Hypothesis layers onto Python's existing test style. Vary integrates property syntax, assertions, generation, and replay into one feature set.

| Concept | Hypothesis | Vary |
|------|------------|------|
| Basic model | A Python test is decorated with `given(...)` and receives generated values from strategies. | A Vary test contains `across(...)` bindings and checks the property with `observe`. |
| Position in the stack | Library-level feature inside Python's testing ecosystem. | Language and compiler feature inside Vary's built-in test DSL. |
| How values are described | You describe generators explicitly with strategies. | You declare typed bindings and Vary generates values from the types. |
| How truth is stated | Usually Python `assert` statements or test-framework assertions. | `observe` is the explicit oracle boundary. |

Hypothesis is stronger when you want rich generator control and need to shape the data until it matches your domain. `across` is stronger when you want less ceremony and want the property to stay visually central. Many useful properties can be written directly from the type system without designing a separate generator.

| Area | Hypothesis | Vary |
|------|------------|------|
| Generator expressiveness | Very mature and central to the user model. | More opinionated and simpler today. |
| Typical authoring style | "Describe strategies, then assert the property." | "Describe the property over typed bindings, then let generation happen." |
| Best fit | Complex data generation and domain-specific sampling. | Straightforward typed properties with low setup overhead. |

Shrinking is where the maturity gap shows most. Hypothesis simplifies a failing example into something closer to the smallest interesting counterexample. Vary now ships shrinking for `across`, but the current system is narrower, focused on simpler runtime value shapes.

Hypothesis also has rule-based state machines: sequences of operations, evolving state, and invariants across transitions. Vary's `across` generates inputs for ordinary test bodies. Good for algebraic laws, parser properties, and round-trip checks, but not yet equivalent to Hypothesis's state-machine layer.

| Deeper capability | Hypothesis | Vary |
|------|------------|------|
| Shrinking | More mature and broader in practice. | Shipped, but currently more limited. |
| Stateful property testing | First-class concept. | Not yet a first-class normal DSL feature. |
| Custom domain generators | Mature and idiomatic. | Still evolving as a user-facing concept. |

Where Vary differs is integration. In Python, Hypothesis is one tool among many. In Vary, [`observe`](/docs/test-dsl/), [`across`](/docs/test-dsl/#property-based-testing-with-across), [contracts](/docs/contracts/), and [`vary mutate`](/docs/mutation/testing/) are designed to work together. Mutation testing asks whether the properties are strong enough to kill real faults.

| Verification concept | Hypothesis | Vary |
|------|------------|------|
| Role of property testing | Explore generated examples inside Python tests. | Part of a broader built-in verification stack. |
| Relationship to assertions | Uses normal assertion mechanisms. | `observe` is a dedicated language construct. |
| Relationship to mutation testing | Usually external or third-party. | Built-in and intentionally connected. |

Hypothesis is more mature and more expressive, especially for strategies, shrinking, and stateful testing. Vary's `across` is more integrated with the language and connects directly to [mutation testing](/docs/mutation/testing/). They solve the same problem from different starting points.

For a narrative introduction to `across`, see [Across the bridge: why three trucks is not enough](/articles/across-the-bridge/).