> so that compilers can reason about it Actually this is the wrong takeaway, I think it's so that programmers can reason about it. This isn't about type error

> so that compilers can reason about it Actually this is the wrong takeaway, I think it's so that programmers can reason about it. This isn't about type errors, it's about precisely describing a particular computational expression. In the python example, it's very unclear what `do_something` actually _does_.