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

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

TypeScript (the types part) absolutely does have ternary operators: https://www.typescriptlang.org/docs/handbook/2/conditional-t...

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

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

> Your type system cannot be sound. It's going to have escape hatches and exceptions because that's how dynamic languages roll. I think you could prove that you can't construct a s…

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…

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

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 …

Espressif's QEMU branch has support for the esp32-c3: https://github.com/espressif/qemu

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

I am the author, feedback welcome.