• [^] # Re: Idris

    Posté par . En réponse à la dépêche Sortie de Coq 8.5 bêta, un assistant de preuve formelle. Évalué à 1.

    Tu as probablement raison, mais je me souviens d'un livre ou un algorithme prouvé 'semi formellement' avait la perle suivant:
    milieu de a,b = (a+b)/2.
    J'avoue que quand j'ai vu ça j'étais mort de rire..