The solution for this might be to add a ME.md in addition to AGENT.md so that it can learn and write down our character, to know if a question is implicitly a command for example.
What should be added, I think, to code reviewing is that it can get really complex, for example if we add formal verification in the mix to catch very subtle bugs.
So in the end I think there will still be some disappointment, as one would expect it should be fully automated and only about reading the code, like this article suggests. In reality, I think it is harder than writing code.
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.
In Rocq/Coq, you have "extraction", which is the standard way to compile programs. This is how the C compiler CompCert is executed, for example. So, all of these languages are in the same category in this respect.
There are RISC-V based zero-knowledge virtual machines, to which a GCC version can be compiled. So this should be possible, although probably very slow, maybe a thousand times slower than a normal GCC execution.
I should add that for pointers to immutable data, we can translate them to immutable values on the Coq side. Thus for Rust code written in a purely functional way (using only immutable data structures) the translation is almost one-to-one with Coq, that is to say the same code up to syntactical differences and the verbosity of our monad that behaves like the identity monad in that case.
Thus we can provide a path for people who are ready to sacrifice performance for proofs. I guess that immutable Rust is simpler to verify with the other systems too.
Yes there is a special primitive for loops in the monad. The primitives are uninterpreted, we define valid finite traces of execution of a program, and reason about these traces.
If a program has a loop we show that it terminates by constructing an execution trace. Note that we do not yet consider concurrency, so programs are deterministic.
No, we have not found bugs! We have only scratched the surface and bugs are probably well hidden as the standard library is very well tested. We do not expect to find bugs there, especially as we also assume the unsafe code is safe.
Our main hope with the translation to Coq of the standard library is to get a formalization of it, so that we can precisely verify Rust programs calling core and alloc.
There are some specifications that are always there, like the absence of reachable panics or the backward compatibility between releases on stable entry points.
Otherwise you can outsource this work to specialized companies such as Formal Land or others!
I do not know how RustHornBelt works. We are focusing on safe code, although we still generate a translation for unsafe blocks as a "best effort".
Compared to Aeneas the goal is very similar as we want to verify Rust programs using interactive theorem provers. However, with coq-of-rust we write the purely functional version of the code (the one on which we make proofs) by hand, or with the help of some GitHub Copilot as this is rather repetitive, and prove it equivalent with the automatic translation. In Aeneas the aim is to directly generate a functional version.
We handle all the pointers as if they were mutable pointers (the `*` type). We do not use any information from Rust's borrow checker, which simplifies the translation, but we pay that at proof time.
To reason about pointers in the proofs, we let the user provide a custom allocator that can be designed depending on how the memory will be used. For example, if the program uses three global mutable variables, the memory can be a record with three entries. These entries are initially `None` to represent when they are not yet allocated. We do not yet know how this technique can scale, but at least we can avoid separation logic reasoning for now. We hope that most of the programs we will verify have a rather "simple" memory discipline, especially on the application side.
The "tedious and error prone" code was what we were doing before, when the translation of the standard library was not yet working automatically with coq-of-rust. Now, this is automatic. Maybe the explanations on the blog post were not clear.
The formalization work for Rust was done mostly at the MIR level, which is one step lower than the THIR level we use here. See, for example, the https://plv.mpi-sws.org/rustbelt/ project. MIR should be more amenable to formal specification, as this language is more compact than THIR and aims to be more stable.
However, we also lose some information going to MIR, as there are no expressions/loops from the original code anymore. There are still ways to reconstruct these, but we preferred to use the THIR representation directly.
The code is translated automatically with coq-of-rust! When issues are found in the translation they can be fixed once in the coq-of-rust tool, and all the translations are updated.
Indeed this would be a nice process to verify coq-of-rust. Also, although the code is rather short, we depend on the Rust compiler to parse and type-check the input Rust code. So that would need to be also verified, or at least formally specified without doing the proofs, and the API of rustc is rather large and unstable. It could still be a way to get more insurance.
I do not think uranium is that expensive, compared to the price of a nuclear reactor itself or other energy sources. I advise to look at wars actually occurring for the control of oil and gas (see country like the US).
At Formal Land we apply formal verification to everyday-life programs. Our key technique is to translate programming code into similar formal Coq code, and do our formal specifications/proofs directly on it. As our main customer, we are formally verifying the implementation of the cryptocurrency Tezos: https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/ This amounts to the verification of around 50,000 lines of code.