[mixedCase]

"All the time" is an english expression, please, look it up before going all-caps Python name mangle convention on me.

Yes, of course dynamic dispatch is a runtime phenomenom, that's the dynamic part of it. But there's nothing stopping the code that performs dynamic dispatch from being strongly typed. Strong types are instructions used to prove that the code holds certain properties, they are a separate program from the final binary the compiler gives you. Do you also think that code that gets unit tested can't perform dynamic dispatch?

If your point is that "types don't exist at runtime anyway" (reflection aside) then you don't understand what the purpose of a type system is, nor what strongly typed code means.

[kortex]

> "All the time" is an english expression, please, look it up before going all-caps Python name mangle convention on me.

I know reaction comments are discouraged on HN, but this had me in stitches. Top-tier gourmet dig right there.

[ukj]

There is something stopping you from running the proof against your implementation!

Proof-checking happens only at compile time.

The implementation that you want to prove things about is only available at runtime!

Non-availability (incompleteness) of information is what is preventing you…