• [^] # coq et transparence

    Posté par . En réponse à la dépêche Mozilla 1.5 disponible aujourd'hui. Évalué à 2.

    Oui.
    Malheureusement on constate régulièrement des bugs dans des puces fondamentales (y compris celles de géants comme Intel) ou dans des logiciels essentiels (y compris des compilateurs C).
    Peut-être que des systèmes de preuves mathématiques comme coq changeront un peu cela...
    A condition aussi d'organiser de manière + simple (et transparente comme l'open-source) les puces et softs essentiels pour limiter les fautes d'inattention qu'on ne pourra jamais totalement exclure !
    http://coq.inria.fr/(...)