Aquí hay una idea divertida que nadie más parece haber mencionado: aprender Coq.
Coq es un “asistente de pruebas”: es un tipo especial de lenguaje de programación que puede usarse para escribir pruebas matemáticas. El sistema verifica tus pruebas para asegurarte de que no cometiste ningún error.
En la práctica, esta no es exactamente la misma habilidad que escribir una prueba matemática normal. ¡Sin embargo, es una muy buena forma de practicar el razonamiento lógico! Tiene algunas ventajas concretas sobre solo intentar escribir pruebas por su cuenta:
- le brinda comentarios inmediatos sobre si su prueba es correcta
- te da más estructura ya que estás limitado por el lenguaje de programación y, por extensión, la lógica en la que estás trabajando
- te obliga a ser aún más preciso : cuando usas Coq, no puedes barrer ningún detalle debajo de la alfombra u olvidar nada
- es interactivo : la herramienta lo ayuda a medida que avanza, haciendo un seguimiento de dónde se encuentra y qué necesita probar
- es divertido
Si te cansas de probar cosas, puedes darte la vuelta y usar Coq como lenguaje de programación normal. Los programas que escriba también vendrán inmediatamente con fuertes garantías sobre la corrección. Puede escribir su programa en Coq y extraerlo en Haskell u OCaml, aunque en este momento es un poco incómodo. Aquí hay un informe interesante de la experiencia de las dificultades involucradas en el uso de este enfoque para escribir un administrador de ventanas: “XMonad en Coq”.
- ¿Por qué el teorema automático es una tarea tan difícil para las computadoras?
- ¿Cómo se demuestra que [matemáticas] 10 ^ {2n-1} +1 [/ matemáticas] es divisible por [matemáticas] 11 [/ matemáticas] mediante inducción?
- ¿Por qué es [matemáticas] \ frac {\ pi} {4} = \ frac {1} {1} – \ frac {1} {3} + \ frac {1} {5} – \ frac {1} {7} + \ cdots = \ sum_ {i = 0} ^ {\ infty} (-1) ^ i \ cdot \ frac {1} {2i + 1} [/ math]?
- ¿Cuáles son algunas pruebas en matemáticas que prueban que ciertas tareas son imposibles?
- ¿Qué metodología se debe adoptar para codificar un programa C libre de errores?
Si bien escribir un programa está aún más alejado de las pruebas matemáticas normales, todavía está profundamente relacionado y sigue siendo una muy buena manera de practicar el pensamiento lógico.