> The reason why people don't use proofs in software development Static types are proofs, and their use is quite widespread. Of course they are "lightweight"

> The reason why people don't use proofs in software development Static types are proofs, and their use is quite widespread. Of course they are "lightweight" proofs driven by program syntax and targeting very general properties, but they're proofs nonetheless. Any claim that "proofs are not used in software dev" has to be heavily qualified to avoid shifting the goalposts.