Langages de programmation fonctionnel ne veut pas dire forcément langage formel prouvable. On ne peut pas tout "prouver" en ocaml.
De plus, la "preuve" concerne un théorème qui correspond à un point de spec, il peut y avoir des oublis ou quelques choses de mal définis. Même un langage "à preuve" ne sera pas sans bug. Et puis dans la pratique, les "prouveurs" automatiques ne passent pas à l'échelle.
[^] # Re: Il ne faut pas confondre l'innovation et le progrès.
Posté par Nicolas Boulay (site web personnel) . En réponse au journal De l'inéluctable progrès de l'informatique, ou pas.. Évalué à 8.
Langages de programmation fonctionnel ne veut pas dire forcément langage formel prouvable. On ne peut pas tout "prouver" en ocaml.
De plus, la "preuve" concerne un théorème qui correspond à un point de spec, il peut y avoir des oublis ou quelques choses de mal définis. Même un langage "à preuve" ne sera pas sans bug. Et puis dans la pratique, les "prouveurs" automatiques ne passent pas à l'échelle.
"La première sécurité est la liberté"