But having every library have type hints means your entire program could be provable. Business logic doesn't make up very much of most applications (at least, n

But having every library have type hints means your entire program could be provable. Business logic doesn't make up very much of most applications (at least, not as much as the libraries it's built on). You're right, though. Python doesn't seem to be made for applications that would benefit from being provably compiled.