어떤 오류가 사소한 실수인가

어떤 오류가 사소한 실수인가

요점

1. 어떤 정의나 증명에 있는 오류가 고치기 쉽더라도 알아차리기 어렵다면, 그 실수는 사소하지 않습니다.
2. 어떤 오류는 증명 보조기의 도움을 받아야 찾아낼 수 있습니다.

간추린 본문

• 지난해 12월부터 올해 4월 16일까지 170시간 정도를 들여 린(Lean) 증명 보조기의 표준 라이브러리에 있는 문자열 정리 String.splitOn_of_valid를 증명했습니다.
• 이 정리를 증명하는 도중에 String.splitOn 함수의 정의에서 버그를 발견했습니다.
• 이 버그를 고치는 일은 그리 어렵지 않았습니다. 해당 정의에서 i를 i - j로 바꾸기만 하면 됐어요.
• 그렇다고 해서 이 오류가 사소한 실수였다고 생각하지는 않습니다. 이 정의에 따르면 splitOn 함수가 대개 올바로 작동하지만, 특수한 경우에는 잘못된 결과를 산출하니까요.
• 린 같은 증명 보조기를 이용하지 않았다면, 이렇게 미묘한 오류를 저는 절대로 못 찾아냈을 것입니다.