[olzd]

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

But you don't have to write a proof to sort a list in Idris. So you're not being honest with your comparison.

[yogthos]

Sure, but then you're not getting the formal guarantees. The whole argument here is regarding whether adding more formalism improves code quality. If you agree that less formalism is better in some cases, then it's just a matter of degrees.