Affirmer publiquement un théorème, en proposer l'usage à autrui et pourtant lui refuser la lecture de la preuve, j'appelle cela se foutre de la gueule du monde !!!
La correspondance de Curry-Howard, à part peut-être dans certains langages spécialisés, est largement théorique. Je ne crois pas que qui que ce soit puisse expliciter le théorème prouvé par le noyau Linux, alors même que le code est disponible et sous GPL.
Et quitte à faire de la patalogique, la preuve est tout aussi bien encodée par le code source que par la forme compilée, donc distribuer la forme compilée uniquement n’est pas « refuser la lecture de la preuve » : la preuve est toujours là.
[^] # Re: Libre de brevets
Posté par Moonz . En réponse à la dépêche FLIF, un format d’image sans perte, intelligent et « performant », sous licence GPL. Évalué à 4.
La correspondance de Curry-Howard, à part peut-être dans certains langages spécialisés, est largement théorique. Je ne crois pas que qui que ce soit puisse expliciter le théorème prouvé par le noyau Linux, alors même que le code est disponible et sous GPL.
Et quitte à faire de la patalogique, la preuve est tout aussi bien encodée par le code source que par la forme compilée, donc distribuer la forme compilée uniquement n’est pas « refuser la lecture de la preuve » : la preuve est toujours là.