Thanks for the theorical background. I just had a look at the Curry-Howard Isomorphism article on Wikipedia, and i finally understood what my OCaml teacher muttered once in the classroom 10 years ago :))
The part i didn't get in the equivalence between program and proof, is that a function can be seen as a proof that provided the input parameters are of a given type, the output type is going to be that one. Quite simple in fact, but it only clicked right now :)
The part i didn't get in the equivalence between program and proof, is that a function can be seen as a proof that provided the input parameters are of a given type, the output type is going to be that one. Quite simple in fact, but it only clicked right now :)