kuruczgy

4 ms·

1.
by kuruczgy 6mo ago
> 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 W
2.
by kuruczgy 1y ago
So Litex is not based on Type Theory I gather. How are proofs represented and checked?
3.
by kuruczgy 1y ago
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 := ...
4.
by kuruczgy 1y ago
TypeScript (the types part) absolutely does have ternary operators: https://www.typescriptlang.org/docs/handbook/2/conditional-t...
5.
by kuruczgy 1y ago
> 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 anywa
6.
by kuruczgy 1y ago
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 s
7.
by kuruczgy 1y ago
> 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 sound & complete type system for Lua. B
8.
by kuruczgy 1y ago
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?)
9.
by kuruczgy 1y ago
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
10.
by kuruczgy 1y ago
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
11.
Porting Lean to the ESP32-C3 RISC-V Microcontroller(kuruczgy.com)
2 points by kuruczgy 2y ago|0 comments
12.
by kuruczgy 2y ago
Espressif's QEMU branch has support for the esp32-c3: https://github.com/espressif/qemu
13.
by kuruczgy 3y ago
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
14.
A formally verified R-tree implementation(kuruczgy.com)
2 points by kuruczgy 3y ago|0 comments
15.
Theorem Proving in Coq(kuruczgy.com)
2 points by kuruczgy 3y ago|0 comments
16.
by kuruczgy 4y ago
I am the author, feedback welcome.