On Sat, Aug 8, 2020, 12:18 AM Ricky Teachey 
Yes, it's hard in the sense that it would require solving the halting problem.

That doesn't sound so hard. ;)  

Thanks for educating me. Could it at least be useful for:

1. Providing semantic meaning to code (but this is probably not enough reason on its own)
2. Couldn't it still be useful for static analysis during runtime? Not in cpython, but when the type hints are used in cython, for example?

Being static like CPython doesn't help. You cannot know statically what the result of an arbitrary computation will be.

There are certainly languages with guards. For example, Python. I can definitely write a function like this:

def small_nums(i: int):
    assert 0 < i < 100

x = small_nums(arbitrary_computation())

In concept, an annotation could be another way to spell an assertion. But I don't think we need that.