En el marco de la correspondencia Curry-Howard o, en términos generales, de las "pruebas como programas", ¿tenemos también "programas como pruebas" y qué demostraría un programa ar

Question

Correspondencia Curry-Howard

Ahora, elija cualquier algoritmo de 5-30 líneas en algún lenguaje de programación de su elección.

¿Qué demuestra el programa? ¿O no tenemos también "programas-como-pruebas"?

Tomemos el algoritmo GCD escrito en pseudocódigo:

function gcd(a, b)
    while b != 0
        t := b
        b := a mod b
        a := t
    return a

¿Qué está demostrando? Pido disculpas por la amplitud y suavidad de esta pregunta, pero realmente me lo estoy preguntando.