Take nothing on its looks; take
everything on evidence. There's no better rule.
(Jaggers) C. Dickens Great Expectations.
Ces assistants souffrent toutefois d'un manque d'automatisation de la recherche de preuve.
L'automatisation est difficile à obtenir dans ce cadre : il ne suffit pas d'obtenir le résultat de procédures de décision automatiques externes, aussi performantes soient-elles. L'assistant refusera en effet de considérer une propriété s'il n'en connait pas de preuve. Celle-ci doit pouvoir être vérifiée par le noyau de certification ; on doit fournir un certificat compréhensible par ce dernier de la preuve de la propriété.
On observe ainsi une séparation entre les assistants qui offrent des garanties formelles de confiance et les outils automatiques performants dont on doit croire les résultats.
Le projet A3PAT souhaite répondre au besoin important de délégation de la preuve de certaines propriétés dans le cadre des techniques liées à la récriture, notamment en définissant des moyens génériques d'exprimer des certificats à la taille raisonnable de propriétés complexes.
Les verrous scientifiques sont à la fois d'ordre théorique et pratique :
À terme, une mise en œuvre des avancées proposées prendra forme à travers le développement d'une nouvelle version de l'outil CiME que nous souhaitons rendre capable de produire des traces vérifiables mécaniquement, par Coq par exemple, des manipulations effectuées et des preuves trouvées.