OCaml Weekly News

We are pleased to share with you Verification for Dummies: SMT and Induction, a complete and detailed series of blogposts written by Adrien Champion about Induction as a formal verification technique.

The subject is treated with many concrete and executable examples. All examples can be (and should be) launched locally by readers thanks to small and easy to find tools. Modification and experimentation are strongly encouraged!

Take a look at all the notions covered:

• introduction to formal logics and formal frameworks;
• SMT-solving: modern, low-level verification building blocks;
• declarative transition systems;
• transition system unrolling;
• BMC and induction proofs over transition systems;
• candidate strengthening.

We hope you enjoy reading and we look forward to your feedback!

The video of @dra27's talk on OPAM is now available: https://youtu.be/RHSdlH4el0g. Thanks so much for the great talk, David! And thanks to everybody who attended! (The video starts a couple of minutes into the talk because yours truly forgot to start recording. D'oh!)

We already have some ideas for the next meeting but if there's a topic that you'd like to hear about or are interested on presenting on, please message me.

0.2.5 is available. This release brings significant user friendly improvements.

There is a new binary called with-dkml.exe. Just plop with-dkml in front of a Windows command that requires access to Unix scripts (ie. with-dkml opam install) and it should just work.

There is now a section called Beyond Basics in the Diskuv OCaml user documentation that walks through:

• the first and second tutorials of Getting Started - Learn OCaml
• the bare Opam essentials you need as a beginner (how to find and select an Opam switch, and how to find and install packages using with-dkml opam install), all without leaving the Command Prompt
• installing Visual Studio Code with the OCaml plugin

Huge thanks to @Butanium who lent me much of his time to validate usability from the perspective of a newcomer. More feedback is always welcome.

Links:

• Installation instructions for the latest version
• Release notes for all versions

PS. You won't need with-dkml most of the time. The Beyond Basics documentation shows how to run Dune and the OCaml native compiler directly from the Visual Studio Command Prompt.

Just FYI, a bugfix release learn-ocaml 0.13.1 has just been tagged and:

• released in GitHub ← see the Release Notes and binaries-assets
• pushed to Docker Hub ← ocamlsf/learn-ocaml being the official distribution of Learn-OCaml
• submitted to OPAM default repository