FP-Syd meeting!

Two talks lined up. Abstracts below.

• Rongmin Lu: The differentiable curry and other misadventures in differentiable programming
• Ben Lippmeier: The Why3 theorem proving framework.

Doors open 6pm, meeting starts 6:30pm.

Ben Lippmeier: 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.