All, A insightful take on the problems of using Coq for formal verification: https://raywang.tech/2017/12/20/Formal-Verification:-The-Gap-between-Perfect-Code-and-Reality/ -- Derek M. Jones Software analysis tel: +44 (0)1252 520667 blog:shape-of-code.coding-guidelines.com