If you have something to talk about then please reply to this message.
Ben Lippmeier: The Why3 theorem proving framework.
Doors open at 6pm, meeting proper starts at 6:30.
Everybody who intends to show up on the night shoud RSVP ASAP to allow our
hosts Atlassian to sort out the catering. People who said they were
going but now find that they can't should likewise update their status.
Cheers,
Ben
The Why3 theorem proving framework
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The Why3 framework provides a programming language WhyML and an IDE that connects to external SMT solvers (automatic theorem provers). WhyML is a dialect of ML that allows one to specify pre and post-conditions for functions, and to define logical theories. When a WhyML program is loaded into the IDE it generates verification conditions for each of the functions, which the user can send to an external solver to verify. In the happy case the solver says your thing is true and your function has no bugs. In the not-so-happy case you can use Why3’s builtin tactics to figure out why either 1) the solver isn’t smart enough to know your thing is true, or 2) your thing was never true to begin with. In the unhappy case the verification condition can be exported to an interactive theorem prover like Coq for manual avian attention. I’ve spent about 4 weeks full time working directly with Why3 and found it quite usable, with only a few rough edges. I’ve managed to formalise some of the key operators provided in a TensorFlow like language, such as max-pool and multidimensional array slicing.