clarus

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!

Thanks for the explanations and all the links!

It shoud be possible. A specific feature of Coq that we use is impredicative Set. I do not know if this is the case in F*.

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.

Thanks for the comment! One of the authors here.

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.

It has been a long time and happy to see you back again!

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).

Formal Land | Proof Engineer | Remote or Paris, France | https://formal.land/

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.

Open roles:

* Coq proof engineer: https://formal.land/assets/files/formal-verification-ocaml-f...

Tech Stack: Coq, OCaml, Haskell, Rust, TypeScript

Twitter: https://twitter.com/LandFoobar

Thanks.

As the server seems down, here is a mirror of the content: https://clarus.github.io/coq-renaming-emails/

(this is mailing list)

Here are some other links related to the discussion:

* wiki, where anyone can add proposals: https://github.com/coq/coq/wiki/Alternative-names

* chat: https://coq.zulipchat.com/#narrow/stream/237655-Miscellaneou...

* forum: https://coq.discourse.group/t/renaming-coq/1264

Yes, it did shut down. Other links related to it:

* wiki, where anyone can add proposals: https://github.com/coq/coq/wiki/Alternative-names

* chat: https://coq.zulipchat.com/#narrow/stream/237655-Miscellaneou...

* forum: https://coq.discourse.group/t/renaming-coq/1264

Quoting the mailing-list (which currently seems down):

Hugo reminds of us of the history of the current logo, which is a reference to the Barcelos Coq from Portugal which Gérard Huet liked, whose shape was drawn by Julien Narboux and adapted/colored for the website by Jean-Marc Notin.

The story seems legit to me, knowing some of the people. I believe there were no jokes in the logo itself, but could be wrong. This was from a time where research projects had many hand-made logos.

This is exactly how drones were used in Syria as I understood. To attack otherwise protected targets or strike fear.

To attack Russian bases they even use swarms of suicide planes: https://www.bellingcat.com/news/mena/2018/01/12/the_poor_man...

Morally not possible.

Before the spread of disposable masks (a few dozens of years back), the masks were made of cloth. Look at the pictures from the 1918 fever for example. I guess studies were made, it would be interesting to know what people thought.

There are some people studying Rust with formal verification. For example in this paper https://plv.mpi-sws.org/rustbelt/rbrlx/paper.pdf However I do not know if the whole language is covered or only a core.

As far as I remember, Git was already going strong at the time GitHub appeared. I was also a supporter of Mercurial at first, but I think Git won because:

* it always was fast (written in C vs Python for Mercurial);

* Linus and Linux are behind it.

Tech is the softest industry ever created.

I am pretty sure that this is the tech people who created this industry and all the jobs evolving around. Softwares are generating a lot of revenue but are incredibly used too.

Pylint and mypy are about syntax and type-checking. While I agree these kind of tools work well, if think that by static analysis people usually imply something which goes farther than that. For example, the languages Facebook is citing (C++, Java, ...) already include type-checking in the compiler.

The fact that Erlang was created for this job does not imply it is the right tool.