> It's true that static type-checking proves the absence of an entire class of errors. But it doesn't prove that the code does the correct thing;

So prove it yourself. Proving things about programs that rely on dynamism is invariably much harder than proving things about programs that don't.