I don't think it is unreasonable to demand confidence from a proof assistant. But some people seem to be saying it is fine to live without the confidence. I am very puzzled about this.
@MartinEscardo While I don't share their opinion, I can imagine it. Not everyone wants proof assistants to add confidence, some people just want them as tools that aid in finding proofs. Similar to how many people currently use computer algebra systems (but in a different way/domain).
Add comment