Questions tagged [bugs]

A software bug is an error, flaw or fault in a computer program or system that causes it to produce an incorrect or unexpected result, or to behave in unintended ways.

Filter by
Sorted by
Tagged with
0 votes
0 answers
51 views

Correcting formally verified results

John Harrison spoke once about checking the results of some peer reviewed mathematical research: he has found bugs in the proofs and even a faulty theorem, which he corrected by giving a formal proof. ...
Gergely's user avatar
  • 299
1 vote
1 answer
80 views

Code obtained from printing a definition from the Lean 3.46 equation compiler does not type check. Why doesn't it, and how can I fix it?

In the example below, the fibonacci function is defined via the Lean equation compiler. However, there seems to be a problem with the code that is obtained from running ...
ttbo's user avatar
  • 35
3 votes
2 answers
371 views

How do you know a formal proof (mechanized within a Proof Assistant) really is correct?

Running a proof assistant as a user and focusing on a given formal proof, how can one assert that there are no unexpected errors or "bugs" that could invalidate the provided proof? More ...
taylor.2317's user avatar
  • 1,308