I did a PhD from 1995 to 1999 under the supervision of Christine Paulin, regarding verification of imperative programs in the system Coq. Right after my PhD, in fall 1999, I redesigned the architecture of Coq, to isolate a kernel ; this is briefly described in this paper. Then I left for a post-doc at SRI, in the PVS team, where I started the development of the ICS decision procedure. When I returned to France, I started in 2001 the development of a tool for program verification called Why, used for the proof of C programs (in the Caduceus tool, now subsumed by Frama-C) and for the proof of Java programs in the Krakatoa tool. In 2010, the Why tool became Why3.