Les développements matériels récents en informatique quantique annoncent des machines de calculs efficaces pour un futur proche. Cette situation appelle au développement d’un génie logiciel consacré à ce paradigme de calcul. Un défi majeur consiste ici au développement de méthodes de débogage et de vérification de code, puisque les stratégies standards (basées sur le test et la vérification d’assertion) sont rendues impuissantes par les lois même de la physique quantique ici à l’œuvre (mesure destructrice, indéterminisme). Fort de son expérience et de son expertise dans les domaines de l’analyse statique et de la vérification formelle de code dans le cas classique, le CEA adapte ces méthodes au cas quantique.
La solution repose sur un langage de programmation quantique associé à une sémantique formelle, permettant :
Ces développements s’appuient sur la technique de vérification déductive, éprouvée dans le cas classique, et sur la représentation symbolique des calculs quantiques comme « sommes de chemins », version discrète des intégrales de chemins proposées par Richard Feynman (cf. figure 2).
L’outil a été éprouvé par le développement entièrement vérifié d’algorithmes quantiques non triviaux, notamment la première implémentation prouvée de l’algorithme de Shor, et place Qbricks au premier rang dans la compétition internationale (cf. figure 3). Il a donné lieu à une publication dans ESOP 2021 ainsi qu’à l’édition d’un chapitre d’ouvrage en 2023.
Les développements en court visent à intégrer Qbricks dans une chaîne complète de développement à usage pratique. Ceci passe notamment par :
Le projet Qbricks se concentre sur le problème du développement sûr et efficace de programmes quantiques, en adaptant au cas quantique les meilleures pratiques classiques en termes de langages, analyse de code et compilation.
Vers des outils de vérification formelle pour une chaîne de développement et de compilation sûre.
