> there is no type system (that I'm aware of, not even Idris as far as I know) which can prove in its static type system every piece of logic about a program.
Many static type systems can prove anything that can be proven. Notionally one might write a program that relies on something unproven like the Collatz conjecture, though I'm not sure that would happen in practice (e.g. it's easy to write a program that relies on the Collantz conjecture for numbers below 2^64, but that's quite provable). Whether it's actually worth writing out the proof is another question though.
> This means that some properties of the system will end up being checked (if you bother to) at runtime and not at compile time. That's where pre/post conditions are useful, they contain information (and in a more deliberate form in cases like the Clojure example) about the properties of the system that are hard or impossible to encode directly in the type system.
This is true but makes surprisingly little difference, because you still want to keep track of which values have or haven't had that runtime check applied. So you almost always want your postconditions expressed as types (even if they're just "marker" types that indicate that a given runtime check was passed). Put another way, any metadata you would want to be able to track about a function's argument values or return value, you almost always want to be able to carry that metadata around with that value before it's passed in or after it's returned - but at that point that metadata is a type, and it's easiest to represent it as one.
Many static type systems can prove anything that can be proven. Notionally one might write a program that relies on something unproven like the Collatz conjecture, though I'm not sure that would happen in practice (e.g. it's easy to write a program that relies on the Collantz conjecture for numbers below 2^64, but that's quite provable). Whether it's actually worth writing out the proof is another question though.
> This means that some properties of the system will end up being checked (if you bother to) at runtime and not at compile time. That's where pre/post conditions are useful, they contain information (and in a more deliberate form in cases like the Clojure example) about the properties of the system that are hard or impossible to encode directly in the type system.
This is true but makes surprisingly little difference, because you still want to keep track of which values have or haven't had that runtime check applied. So you almost always want your postconditions expressed as types (even if they're just "marker" types that indicate that a given runtime check was passed). Put another way, any metadata you would want to be able to track about a function's argument values or return value, you almost always want to be able to carry that metadata around with that value before it's passed in or after it's returned - but at that point that metadata is a type, and it's easiest to represent it as one.