David Dill, Novi Research
Série de séminaires de recherche sur la blockchain
Résumé : La blockchain Libra, initiée en 2018 par Facebook, comprend un nouveau langage de programmation appelé Move pour la mise en œuvre de contrats intelligents. La correction des programmes Move est particulièrement importante car la blockchain hébergera de grandes quantités d'actifs, ces actifs étant gérés par des contrats intelligents, et en raison d'un historique de pertes importantes sur d'autres blockchains à cause de bugs dans les contrats intelligents. Le langage Move est conçu pour être aussi sûr que possible, et il est accompagné d'une spécification formelle et d'un outil de vérification automatique, appelé Move Prover. Un projet visant à spécifier et à vérifier formellement autant de propriétés importantes que possible de la bibliothèque standard Move est désormais bien avancé.
Cette présentation portera sur les objectifs du projet et les idées les plus intéressantes que nous avons eues jusqu'à présent.