This is really impressive work. Formally proving programs correct is especially hard when there are pointers. This approach manages to handle them, without ev

This is really impressive work. Formally proving programs correct is especially hard when there are pointers. This approach manages to handle them, without even requiring special programmer annotations like Rust requires. I'm a big fan of the Why3 / ProVal / Toccata approach. Instead of building one tool to do everything, they've broken things down so they can support multiple programming languages (C / Java / Ada / Why's ML variant), multiple automated provers (e.g., Z3, alt-ergo), and multiple interactive provers (Coq, Isabelle). It seems to be a very promising approach. Cool! Thanks for sharing!