Safety and Correctness
Much like Rust's type system helps ensure memory safety, Hydro helps ensure distributed safety. Hydro's type system helps you avoid many kinds of distributed systems bugs, including:
- Non-determinism due to message delays (which affect arrival order), interleaving across streams (which affect order of handling) or retries (which result in duplicates)
- Observing a collection that is still asynchronously changing as if it were a final result
- Using mismatched serialization and deserialization formats across services
- Misusing node identifiers across logically independent clusters of machines
- Relying on non-deterministic clocks for batching events
These safety guarantees are surfaced through the Rust type system, so you can catch these bugs at compile time rather than in production. And when it is necessary to bypass these checks for advanced distributed logic, Hydro requires you to attach non-determinism guards that explain the effects of the non-determinism, clearly marking the code that should be carefully reviewed.
Some APIs are only deterministic if the closures you pass them satisfy algebraic properties, such as commutativity for aggregations over unordered streams. Hydro requires these to be backed by proofs: either a written manual_proof! or a proof that is machine-checked by Verus.