I believe software has the potential to be an exception of "any human endeavor done at scale is going to be a complete clusterfuck of a trainwreck." In software

I believe software has the potential to be an exception of "any human endeavor done at scale is going to be a complete clusterfuck of a trainwreck." In software development, there are methods to scale correctness not mistakes, but they are not as prevalently used as desired. Some practical examples being: 1. Affine types in Rust. 2. Refinement types in Ada. 3. Dependent types in Coq/Agda/Lean/Idris/ATS-lang. 4. Separation logic in Facebook Infer. These methods systematically/automatically eradicate errors that incomprehensive/human-intensive alternatives (unit-testing, code review) can't do at scale. If our industry could adopt and improve on this, we could create truly ambitious projects with confidence, at a lower cost, and at a faster pace because 1) correctness is scaled and 2) mistakes are contained.