How do you know if a Proof Assistant is working in the correct manner? This came up in the review queue to reopen. I replied with keep closed for original reasons.
I would have liked to add a comment to explain why so will do here. The part I have a problem with is that the question notes When running / using a proof assistant A proof assistant released to users should not have bugs in the proof engine. How that is determined is a different question.
@HenryWHHackv3.0b Why not comment on the post itself? The question is closed. I don't know if everyone can see the comments. What I don't get is why the review process doesn't allow for comments on any review. It seems it only allows for user text entry for certain reason.
@HenryWHHackv3.0b Or ping the original poster in the Proof Assistants Stack Exchange main chatroom. Oops Wrong room. Like I said many times, SE Chat drives me nuts.
@HenryWHHackv3.0b People can still see comments on closed posts. What I should have said is the questions is closed. I don't think every one can see closed questions and the associated comments.
When running / using a proof assistant as a user, how can you check that there are no errors / bugs that may provide an incorrect output?
e.g. if I asked what type of sum 1+1 is and it said "Multiplication".
What could a user do to check everything at once?
It was just turning into lines getting worse and worse. Also as I try to delete all, and I mean all, of my comments here, those were just an exception I was tired of working around. On StackOverflow I have pages and pages of comments and would delete them all but it could take days. Deleting these everyday keeps me focused on not adding useless comments that I will have to delete again.
@Wno-all I really would like to see a site that shows different proofs done using different proof engines. I say proof engines because I am indifferent if the proof generated via automation, person or a combination.
@Wno-all However I thought of another reason why those type of questions should not be on this site. On the golf site the answers are typically not given accept votes. So the stats for that site can not be compared to other sites because it is apples to oranges. If those questions are here and I would expect those questions not to be awarded an except vote, then this sites stats will be thrown into disarray. (I really do hate SE chat. It is a pain in the a--).