Viewing profile — 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 …

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 …

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 t…

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 slow…

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 immut…

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. I…

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, e…

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 o…

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 ve…

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 auto…

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/ p…

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 …

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 …

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 transla…

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:…

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/#narro…

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 …

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:…