La problématique première lors du design d’un langage de programmation est traditionnellement l’expressivité en termes de description d’algorithmes et d’architecture. Rares sont ceux qui se soucient de la question de la spécification logicielle ou de la vérification. Et pourtant. On ne compte plus les coupures de presse annonçant pertes abyssales ou trous de sécurité béants laissés ouverts par des défauts de programmation souvent primaires. Le législateur logiciel contraint de plus en plus d’industries à des phases de tests et de relecture de code si étendues qu’elles accaparent le plus gros des ressources de développement. Dans ces domaines, toute l’aide que peut apporter le formalisme logiciel est la bienvenue. La clef de voute de la fiabilité que nous allons présenter ici, c’est la spécification. En particulier dans sa capacité à exprimer des propriétés sur le code sous forme d’assertions vérifiables : le contrat.