On the occasion of the 68th birthday of the Flag of Europe, we are delighted to release the version 1.0 of CAISAR. The release source is available under our gitlab. It will soon be available on opam and on Dockerhub.
We extended the WhyML specification language to take into account common machine learning constructs. It is now possible to model machine learning computations using vectors and datasets. Parts of this specification can be interpreted directly by CAISAR. CAISAR can then instanciate the specification with concrete values provided by the user. CAISAR can also compute the results of operations on vectors such as getting an index on a concrete vector, or normalizing a dataset. Finally, this language allows to perform transformations on the proof goals that makes them more amenable for provers.
The end result is a cleaner modelling language that behaves “as expected” for the user, bridging the gap between the specification and the actual system. We believe that this will surely be helpful for the community.
Check the updated documentation examples to get a grasp on the new language.
It is now possible to specify which theories and/or goals to check within a specification. CAISAR is now available as a Nix flake. We plan to make it available on nixpkgs in a future release. We added a contribution guide in the manual, under the contributing section.