A new extraction system from Rocq to functional-style, memory-safe, thread-safe, readable, valid, performant, and modern C++.
Interestingly, this can be integrated into production system to quickly formally verify critical components while being fully compatible with the existing Bloomberg's C++ codebase.
Would be interesting to see how performant it is (or how easily you can write performant code).
This is ... okay, if you like formal systems, but I wouldn't call it performant. Depending on what you are doing, this might be performant. It might be performant compared to other formally verified alternatives. It's certainly a lot nicer than trying to verify something already written in C++, which is just messy.
From theories/Mapping/NatIntStd.v:
- Since [int] is bounded while [nat] is (theoretically) infinite,
you have to make sure by yourself that your program will not
manipulate numbers greater than [max_int]. Otherwise you should
consider the translation of [nat] into [big_int].
One of the things formal verification people complain about is that ARM doesn't have a standard memory model, or CPU cache coherence is hard to model. I don't think that's what this project is about. This project is having basically provable code. They also say this in their wiki:
> Crane deliberately does not start from a fully verified compiler pipeline in the style of CompCert.
What this means is that you can formalize things, and you can have assurances, but then sometimes things may still break in weird ways if you do weird things? Well, that happens no matter what you do. This is a noble effort bridging two worlds. It's cool. It's refreshing to see a "simpler" approach. Get some of the benefits of formal verification without all the hassle.
A new extraction system from Rocq to functional-style, memory-safe, thread-safe, readable, valid, performant, and modern C++.
Interestingly, this can be integrated into production system to quickly formally verify critical components while being fully compatible with the existing Bloomberg's C++ codebase.
Would be interesting to see how performant it is (or how easily you can write performant code).
From tests/basics/levenshtein/levenshtein.cpp:
This is ... okay, if you like formal systems, but I wouldn't call it performant. Depending on what you are doing, this might be performant. It might be performant compared to other formally verified alternatives. It's certainly a lot nicer than trying to verify something already written in C++, which is just messy.From theories/Mapping/NatIntStd.v:
One of the things formal verification people complain about is that ARM doesn't have a standard memory model, or CPU cache coherence is hard to model. I don't think that's what this project is about. This project is having basically provable code. They also say this in their wiki:https://github.com/bloomberg/crane/wiki/Design-Principles#4-...
> Crane deliberately does not start from a fully verified compiler pipeline in the style of CompCert.
What this means is that you can formalize things, and you can have assurances, but then sometimes things may still break in weird ways if you do weird things? Well, that happens no matter what you do. This is a noble effort bridging two worlds. It's cool. It's refreshing to see a "simpler" approach. Get some of the benefits of formal verification without all the hassle.