Je dirai où en est PML, notamment, l'algorithme de typage et le proof-checking. Je montrerai les premiers exemples de programmes prouvés en PML.