clarus

9 ms·

1.
by clarus 20d ago
Thanks for the links! There is also Upkie: https://github.com/upkie/upkie
2.
by clarus 6mo ago
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.
3.
by clarus 8mo ago
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
4.
Extracting verified C++ from the Rocq theorem prover at Bloomberg(bloomberg.github.io)
129 points by clarus 8mo ago|39 comments
5.
by clarus 8mo ago
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
6.
by clarus 2y ago
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.
7.
by clarus 2y ago
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.
8.
by clarus 2y ago
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 w
9.
by clarus 2y ago
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 constru
10.
by clarus 2y ago
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 mai
11.
by clarus 2y ago
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 L
12.
by clarus 2y ago
Thanks for the explanations and all the links!
13.
by clarus 2y ago
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*.
14.
by clarus 2y ago
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 usin
15.
by clarus 2y ago
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 w
16.
by clarus 2y ago
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
17.
by clarus 2y ago
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.
18.
by clarus 2y ago
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 n
19.
by clarus 4y ago
It has been a long time and happy to see you back again!
20.
by clarus 5y ago
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).
21.
by clarus 5y ago
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 Co
22.
by clarus 5y ago
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 proposal
23.
by clarus 5y ago
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/strea
24.
by clarus 5y ago
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 a
25.
by clarus 6y ago
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&#
26.
by clarus 6y ago
Morally not possible.
27.
by clarus 6y ago
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.
28.
by clarus 7y ago
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.
29.
by clarus 7y ago
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 be
30.
by clarus 7y ago
> 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.

More ›