Xavier Leroy on programming, languages and formal verification