Welcher Fehler ist ein trivialer Irrtum?
Kerngedanken
- Wenn sich ein Fehler in einer Definition oder einem Beweis zwar leicht beheben lässt, aber schwer zu entdecken ist, dann ist dieser Irrtum nicht trivial.
- Manche Fehler lassen sich nur mithilfe eines Proof Assistants finden.
Kurzfassung
- Von letztem Dezember bis zum 16. April dieses Jahres habe ich rund 170 Stunden darauf verwendet, den String-Theorem
String.splitOn_of_valid in der Standardbibliothek des Lean-Proof-Assistants zu beweisen.
- Während ich dieses Theorem bewies, entdeckte ich einen Bug in der Definition der Funktion
String.splitOn.
- Diesen Bug zu beheben war nicht besonders schwierig. In der betreffenden Definition musste lediglich
i durch i - j ersetzt werden.
- Trotzdem halte ich diesen Fehler nicht für einen trivialen Irrtum. Nach dieser Definition funktioniert die Funktion
splitOn meist korrekt, liefert aber in Sonderfällen ein falsches Ergebnis.
- Ohne einen Proof Assistant wie Lean hätte ich einen derart subtilen Fehler niemals finden können.
Noch keine Kommentare.