Comment by brokencode

That’s the dream with dependent type systems, but from my very limited exposure to them, it seems like it’d be very difficult to encode complex constraints like all of your company’s business logic in this way.

Not saying it can’t be done, but I think it’s a bit telling that no such language has ever caught on.

Unit testing can also be used to verify such constraints and is much simpler. It obviously doesn’t guarantee correct behavior like a proof, but if the tests are comprehensive, it can do a great job.