Comment by naasking

> Sorry if this is obvious, but do these languages let programmers explicitly assert that a certain, relevant property holds at runtime?

You can assert something but then you also have to prove it. An assertion is like a type declaration: you're asserting values of this type can exist. The proof of that assertion is constructing a value of that type to show that it can be instantiated.

This is what the Curry-Howard correspondence means. The types of most languages are just very weak propositions/assertions, but dependent types let you declare arbitrarily complex assertions. Constructing values of such arbitrarily complex assertions can get very hairy.