Title: A fresh approach to program proving (from Ada to machine code)