Really? What language allows you to encode business logic into its type system?

I'm talking about things like, what happens if you press this button; is this calculation correct; does this lookup give me the desired results; does X get stored in the database correctly (or retrieved from it); etc. I don't know of any type system that lets you check these things.

(Also, I assume s/strongly/statically; Python is a strongly typed language. Granted, not everybody agrees about the terminology...)