My hunch is that tools like TLA+ and Lean[0] are bringing down the total cost of developing more reliable software. And developing software that is reliable sh

My hunch is that tools like TLA+ and Lean[0] are bringing down the total cost of developing more reliable software. And developing software that is reliable shouldn't be relegated to the safety-critical applications. There are ways that software failures can still cause significant harm even without putting human lives at risk: security errors allowing bad actors to steal personally identifying information, funds, or otherwise disrupt services that could harm people. This costs people their livelihoods, affects insurance rates for everyone, etc, etc. I think the software industry needs to be more accountable for the influence we're having over the lives of the public and in order to write more secure, safer systems we need better tools to check our specifications, constrain our implementations, and help us manage complexity. [0] https://leanprover.github.io/ https://leanprover.github.io/