Show HN: B01T – What if quantum computing had Rust-style safety guarantees?

Category: ai-ml

Tags: quantum-computing, formal-verification, dsl, type-safety

Score: 6.3/10 (Innovation: 8, Technical: 7, Documentation: 6, Utility: 4)

b01t is a Python DSL for quantum programming that enforces safety guarantees at build time, catching common quantum bugs like dirty ancillae and bad uncomputation. It's interesting because it applies formal verification (machine-checked in Lean 4) to prove quantum programs are unitary channels, a novel approach compared to existing frameworks.

Target audience: quantum researchers, quantum algorithm developers

Repository: https://shukla.io/blog/2026-04/b01t.html · Python · Apache-2.0

View on Hacker News