Article URL: https://github.com/cmk/connections Comments URL: https://news.ycombinator.com/item?id=48936803 Points: 16 # Comments: 1

Galois connections as first-class Rust values. Use them to cast lawfully between numeric types, and compose ladders of conversions whose round-trip behavior is determined by simple inequalities rather than left to chance. Every operation derived from a Conn (rounding, saturation, median, ...) carries a property-tested invariant. The generated fixed-width integer, Q-format, NonZero, and iso families also have Kani harnesses for full bit-width SMT proofs; float SMT coverage is narrower and called out under Testing → SMT verification. MSRV: Rust 1.88. Bumps to the MSRV will be treated as minor-version changes — pin connections = "0.1" and an MSRV upgrade will surface as a 0.2 release rather than a silent break on a patch update. Galois connections are the right shape for static, lawful conversions between partially ordered types (e.g. f64 → f32, Duration → seconds, f32 → u32 → IpAddr, etc) where each link in the chain is specifiable at compile time. The standard cast operators as, From, and Into give you exactly one direction at a time — and as in particular is silent on rounding, saturation, and lossy conversion. Two concrete things this crate gives you that the standard tools don't: (x as f32) as f64 != x for many x: f64. With a Conn, at least one of the following pairs of inequalities is property-tested for every connection in this crate: A Conn is Copy, const-constructible, heap-free, and the crate is #![forbid(unsafe_code)]. The compose! macro folds a chain of pairwise Conns into one fresh Conn<Src, Dst> at compile time. A composed Conn obeys the same properties as its component connections by construction. A Galois connection between preorders A and B is a pair of monotone maps f: A → B and g: B → A such that f(x) ≤ y ⇔ x ≤ g(y). We say f is the left or lower adjoint, and g is the right or upper adjoint of the connection.