Determinism isn't the main hurdle. It would be a moderate effort to engineer a deterministic claude that would be no more useful than the current one.
The key characteristic of a compiler is that it takes a source language with a well-defined meaning to a target language with a well-defined meaning.
The reason claude fails to be a compiler is that its input language (english) can't be precisely defined. (And even if that were possible, it would very often fail to preserve the meaning when "compiling")
This is a case of lethal trifecta. This particular one can be fixed by either not giving the AI private data, or by removing the exfiltration opportunity. Why does the comment-summary bot need access to your private video ids? Why does it need to be able to output links?
Most cases of prompt injection are harder to fix, and the success of the products they occur in relies on engineers who should know better sticking their heads in the sand about security risks.
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++.
The key characteristic of a compiler is that it takes a source language with a well-defined meaning to a target language with a well-defined meaning.
The reason claude fails to be a compiler is that its input language (english) can't be precisely defined. (And even if that were possible, it would very often fail to preserve the meaning when "compiling")