You'd see it at run-time, but most likely at test-time. Which is not a "time" we often think about.
Spec is designed so that you setup automated generative tests on your specced functions. These perform brute force search of the input space.
So, they won't give you FOR ALL guarantees, but will still catch quite a lot. For functions with small input domains, it would actually prove FOR ALL.
The trade off is that, you can test for much more. You can test for properties of the values, not just type. Like say making sure that the output is always smaller than the input. Or that the input never is a blank or empty string.
A downside, it doesn't work well for unpure functions. Since the generative brute force doesn't have a way to brute force the side effect, or assert properties about it. For those, you'd need to write your own tests.
All in all, don't expect it to be at all like a static type checker. It's a very different beast, which you'll want to use very differently, and which offers a very different value proposition. For example, you could want to use Spec even if you had a static type system. Just like people still write tests. Spec is a new kind of tool that can be leveraged to mitigate software defects.
Spec is designed so that you setup automated generative tests on your specced functions. These perform brute force search of the input space.
So, they won't give you FOR ALL guarantees, but will still catch quite a lot. For functions with small input domains, it would actually prove FOR ALL.
The trade off is that, you can test for much more. You can test for properties of the values, not just type. Like say making sure that the output is always smaller than the input. Or that the input never is a blank or empty string.
A downside, it doesn't work well for unpure functions. Since the generative brute force doesn't have a way to brute force the side effect, or assert properties about it. For those, you'd need to write your own tests.
All in all, don't expect it to be at all like a static type checker. It's a very different beast, which you'll want to use very differently, and which offers a very different value proposition. For example, you could want to use Spec even if you had a static type system. Just like people still write tests. Spec is a new kind of tool that can be leveraged to mitigate software defects.