SQL fait ses preuves

Véronique Benzaken, équipe VALS, LRI, université Paris-Sud Orsay

Les données sont omniprésentes et précieuses. De façon surprenante peu d’attention a été consacrée pour garantir, de manière indiscutable, que les systèmes en charge de leurs traitements sont sûrs. Une approche prometteuse afin d’obtenir des garanties fortes est d’utiliser des assistants à la preuve tels que Coq.

Dans cette conférence nous nous intéresserons aux systèmes relationnels qui sont parmi les plus répandus et tout particulièrement à la chaîne de compilation de SQL. Nous décrirons les différentes étapes indispensables à l’obtention d’une chaîne de compilation certifiée : spécification extrême, en Coq, du modèle relationnel, mécanisation, en Coq, de la sémantique de SQL, analyse syntaxique et sémantique certifiée et optimisation vérifiée.

Si SQL est l’un des langages les plus utilisé dans le monde — il est seulement dépassé par Javascript et figure loin devant C et C++ — c’est aussi l’un des langages le plus redouté et le moins apprécié des programmeurs. Nous tenterons, au cours de la présentation, d’expliquer, à la lumière implacable portée par Coq, pourquoi.