Hacker News new | past | comments | ask | show | jobs | submit login

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




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: