> (For what it’s worth, if you use a prover-adjacent language such as Agda or Idris, this is exactly how things are going to work there.) You don't even have t

> (For what it’s worth, if you use a prover-adjacent language such as Agda or Idris, this is exactly how things are going to work there.) You don't even have to go that far, Rust supports this concept. The built-in empty type is called `!`, and cannot be constructed. It's partially unstable, and there's a bunch of things you can't do yet, but you can use it as a return type.