Yeah, you need dependent typing to do that in a programming language. But as cool as dependently typed languages are, developing serious software in them remain

Yeah, you need dependent typing to do that in a programming language. But as cool as dependently typed languages are, developing serious software in them remains a bit of a research problem. Idris is closest, but it also less convenient for actual proofs.