Qué error es un descuido menor

Qué error es un descuido menor

Puntos clave

1. Si un error en una definición o demostración es difícil de detectar aunque sea fácil de corregir, entonces ese error no es menor.
2. Algunos errores solo pueden encontrarse con la ayuda de un asistente de pruebas.

Resumen del texto

• Desde diciembre del año pasado hasta el 16 de abril de este año, dediqué unas 170 horas a demostrar el teorema String.splitOn_of_valid de la biblioteca estándar del asistente de pruebas Lean.
• Mientras demostraba este teorema, encontré un bug en la definición de la función String.splitOn.
• Corregir este bug no fue especialmente difícil. Solo había que cambiar i por i - j en esa definición.
• Pero eso no significa que este error haya sido un descuido menor. Según esa definición, la función splitOn suele funcionar correctamente, pero en casos especiales produce resultados incorrectos.
• Si no hubiera usado un asistente de pruebas como Lean, nunca habría podido encontrar un error tan sutil.