<warning type="approximations">
On ne peut pas tout prouver (en particulier, on ne peut prouver aucune propriété non triviale d'une machine de Turing si je ne dis pas de connerie), mais on peut prouver que la machine virtuelle (ou un programme en général) répond bien à certaines spécifications. C'est le domaine de la certification logicielle, ça utilise essentiellement de la logique, et effectivement on a de jolis résultats théoriques parfois un peu galères à mettre en pratique (notamment parce que les démonstrations ne sont que rarement automatiques, en général semi-automatiques).
</warning>
[^] # Re: [X] : C'est exactement ce que j'espérais
Posté par MrLapinot (site web personnel) . En réponse au journal Sondage Java sous GPL, donnez votre avis à Sun. Évalué à 1.
On ne peut pas tout prouver (en particulier, on ne peut prouver aucune propriété non triviale d'une machine de Turing si je ne dis pas de connerie), mais on peut prouver que la machine virtuelle (ou un programme en général) répond bien à certaines spécifications. C'est le domaine de la certification logicielle, ça utilise essentiellement de la logique, et effectivement on a de jolis résultats théoriques parfois un peu galères à mettre en pratique (notamment parce que les démonstrations ne sont que rarement automatiques, en général semi-automatiques).
</warning>
Merci de corriger les bêtises.