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.
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!