Hacker News new | ask | show | jobs
by antpls 2913 days ago
A theorem prover let you prove that your code is bug free in some cases. Why not use a theorem prover for your specifications too?
1 comments

Because only a human can decide whether the specification matches the intent. This is not a hard concept. The machine can only tell you that your specification is self-consistent, not that it's specifying what you wanted.
The machine could go a level above and helps the human to reflect about its intents. That would basically be a machine convincing the human he/she is already happy right now, and he/she doesn't need to earn more money, and therefore doesn't need that "new e-commerce website". An artificial psychologist conversational agent would help you know about what you really want in life :)
:)