I guess it could be very uncomfortable to use a theorem prover that is not open-... | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		gosub on April 13, 2012 \| parent \| context \| favorite \| on: Rise4fun - from Microsoft Research I guess it could be very uncomfortable to use a theorem prover that is not open-source, especially if your work is at stake. Closed-sourceness abruptly cuts the chain of trust at Microsoft.

ot on April 13, 2012 [–]

You don't have to trust a theorem prover, it gives you either a proof or a counter-example. You can use another tool to verify them.

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