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

That's the thing - I'm not talking about using any mechanical checkers. I'm talking about using a language definition that makes it easier for humans to prove things about their programs.

Okay, that's interesting. How would that work in practice? It doesn't seem like it would be easy to apply in a timely way. If the rules can be unambiguously checked by humans, would they not be more efficiently checked by machines?

Proving theorems isn't just performing routine checks. There are creative aspects, like finding the right loop invariants, at which machines fare absolutely miserably.

OTOH, machines excel at exhaustive enumeration and enforcing separation of concerns: that's why ML-style algebraic data types, pattern matching and parametric polymorphism are such a boon for high-level programming.

So there's room for both human and machine work in program verification. What we should be interested in is finding the right division of labor between humans and machines.

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