> 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.
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.