[pka]

> Reading and understanding the Idris proof is actually more work than understanding the untyped Python version, therefore it's actually harder to say whether it's correct or not in a semantic sense.

That was your original, nonsensical, point (emphasis mine).

> My point is that tests and runtime contracts provide sufficient guarantees in practice.

That's your revised point (which I don't care much about discussing), after moving the goalposts sufficiently.