kuruczgy

> It’s important to note that this is the Lean runtime that has a bug, not the Lean kernel, which is the part that actually does the verification (aka proving). [1] So it’s not even immediately clear what this bug would really apply to

Well, Lean is written in Lean, so I am pretty sure a runtime bug like this could be exploited to prove `False`. Yes, since the kernel is written in C++, technically it's not the part affected by this bug, but since you cannot use the Lean kernel without the Lean compiler, this difference does not matter.

So Litex is not based on Type Theory I gather. How are proofs represented and checked?

Well, if your language has a sufficiently strong type system (namely, dependent types), you can take proofs of some properties as arguments. Example in Lean:

  def clamp (value min max : Float) {H : min < max} : Float := ...

> but language models frequently outperform us in reasoning

what

99% of the time their reasoning is laughable. Or even if their reasoning is on the right track, they often just ignore it in the final answer, and do the stupid thing anyway.

Thanks for the detailed answer! I just wish the website was more upfront about this. I cannot find anything about "soundness" on the front page or in the docs.

I think you could basically copy your comment into an FAQ section or something on the front page.

How confident are you in the soundness of the type system?

Also, are there any Lua constructs that are difficult/impossible to type?

Is type checking decidable? (Is the type system Turing complete?)

Yes you are right, what I am proposing is not a solution by itself, it's just a way to be reasonably confident that _if you audit the code_, that's going to be the actual logic running on your computer.

(I don't get the value of your AST checksumming idea over just checksumming the source text, which is what almost all distro packages do. I think the number of changes that change the code but not the AST are negligible. If the code (and AST) is changed, you have to audit the diff no matter what.)

The more interesting question that does not have a single good answer is how to do the auditing. In almost all cases right now the only metric you have is "how much you trust upstream", in very few cases is actually reading through all the code and changes viable. I like to look at how upstream does their auditing of changes, e.g. how they do code review and how clean is their VCS history (so that _if_ you discover something fishy in the code, there is a clean audit trail of where that piece of code came from).

Actually this is not quite true, in the xz hack part of the malicious code was in generated files only present in the release tarball.

When I personally package stuff using Nix, I go out of my way to build everything from source as much as possible. E.g. if some repo contains checked in generated files, I prefer to delete and regenerate them. It's nice that Nix makes adding extra build steps like this easy. I think most of the time the motivation for having generated files in repos (or release tarballs) is the limitations of various build systems.

Looks very promising. I was planning on writing something similar in the past, it's astonishing to me how little people who use git daily actually understand it. Interactive rebasing, for example, is a foreign concept to most, while in my opinion it's a central tool for using git. The fundamentals are also important, again I don't know how people use git daily without actually knowing for example what a commit is. (People have fuzzy concepts like it's a diff (bad), some sort of compressed snapshot (slightly better), but very few have the correct mental model of "a commit is a reference to N parents, a tree, plus some metadata, and the commit hash is simply the hash of all these combined".)

Looking forward to sharing this with colleagues. On one hand I am excited because I think this bottom-up approach is the correct way of understanding git, on the other hand I am afraid that they will think it's difficult to understand and just not bother. (Again I can't fathom how programmers, who you know, learned programming, which is quite a steep learning curve in itself for first time, shy away from learning git properly, a tool that's just as important to their daily work as whatever programming language they are using.)