← Back to context

Comment by nextaccountic

1 day ago

The tool may malfunction. Indeed there are theorems that say the tool must malfunction at least sometimes.

If you don't understand the subject and relies on the understanding of the tool, how will you have a frigging chance of catching an error?

Anyway this reminds me that scene in Matrix 2, where the mayor (of sorts, don't remember his exact title) of Zion tells Neo about the machines that keeps everyone alive, but that there is nobody left that understands how they work or could repair them if they broke.

>Indeed there are theorems that say the tool must malfunction at least sometimes.

Gödel's incompleteness theorem only states that there are true statements that can never be proved to be true. That limits what tools can do, but it's not a "malfunction". The exact same limitation applies to humans. A genuine malfunction would be if the tool "proved" a false statement to be true. That actually has happened before because of bugs in proof checkers, but software bugs can be found and fixed, and proof checkers are simple enough that it's possible to write many different implementations. It's extraordinarily unlikely that the same malfunction occurs in all of them.