Sadly, I suspect this will be the best piece of marketing they could ever hope for. "It's so advanced the government made us add extra security* to stop hackers!"
Here's the threat model I (a luddite) use to evaluate these. The claude code harness can be mostly trusted, the model cannot be trusted because it is exposed to untrusted data from the internet, and there is no separation of data/code in an llm [0][1].
I want to avoid running untrusted code on my local machine, because it could steal secrets, install malware, etc.
Since the model is allowed to write without restriction (I think) to the project directory, anything in the project directory is also untrusted. Running standard commands from the system is fine, as long as you know what those commands are going to do. Running anything from the local directory should be avoided because the code is untrusted.
This is just one security model, there are many others! If a person is running claude in a stronger sandbox, that changes the model considerably. What threat model do you use to evaluate whether an agent's actions are safe?
I think that's selling the theorems a little short. A math system with arithmetic is equal to, or more powerful than, a computer. For an example, even classical logic comes with the law of excluded middle that can say (internally) if a program halts or not. Incompleteness applies to all the stronger systems as well.
They're not doing so here, but shipping a wasm-compiled binary with npm that uses node's WASI API is a really easy way to ship a cross-platform CLI utility. Just needs ~20 lines of JS wrapping it to set up the args and file system.
That's essentially correct. Extraction is a term in roqc. A rocq program contains both a computational part, and proofs about that computation, all mixed together in the type system. Extraction is the automated process of discarding the proofs and writing out the computational component to a more conventional (and probably more efficient) programming language.
The original extractor was to ocaml, and this is a new extractor to c++.
Is early termination the only supported side effect? Its name suggests a more general capability, but I didn't see more examples in my (cursory) look at the readme
Not saying if the title is good or bad, but just to provide context: there's a tradition of these style of apple-language explainers / cheat sheets titled in this pattern. First I'm aware of is https://fuckingblocksyntax.com/ . There seem to be at least 15 of them listed on https://fuckingsyntaxsite.com/ , and probably more with different swears. It's a genre of titles in the same vein as "considered harmful" or "falsehoods programmers believe about"