Vous écrivez que "Le système d'exploitation seL4 [est] prouvé de bout en bout". Je comprends bien ce que signifie "prouver une formule logique", mais qu'entendez-vous par "prouver le système d'exploitation seL4" (seL4 n'est pas une formule logique) ? Et qu'est qu'une preuve "de bout en bout" ?
# seL4 prouvé de bout en bout ! quésaco ?
Posté par coqueux . En réponse à la dépêche Sortie de Coq 8.5 bêta, un assistant de preuve formelle. Évalué à 0.
Vous écrivez que "Le système d'exploitation seL4 [est] prouvé de bout en bout". Je comprends bien ce que signifie "prouver une formule logique", mais qu'entendez-vous par "prouver le système d'exploitation seL4" (seL4 n'est pas une formule logique) ? Et qu'est qu'une preuve "de bout en bout" ?