gopiandcode

7 ms·

1.
Kernel accepts wrong-structure projections, allowing axiom-free proof of False(github.com)
5 points by gopiandcode 2mo ago|0 comments
2.
Using LLM-Based Verification to Eliminate Bugs in Linux's Network Stack(basis.ai)
4 points by gopiandcode 2mo ago|0 comments
3.
Pact: Trustworthy Coordination for Multi-Agentic Ecosystems(basis.ai)
3 points by gopiandcode 5mo ago|0 comments
4.
by gopiandcode 5mo ago
> an untyped closure-based programming language with a similar array and sort api to JS Ah! You're talking about Racket or Scheme! ``` > (sort '(3 1 2) (lambda (a b) (< a b))) '(1,2,3) ``` I suppose you ought to go a
5.
Building an Unverified Compiler with Agents(basis.ai)
2 points by gopiandcode 5mo ago|0 comments
6.
by gopiandcode 5mo ago
If you're pushing me, let's say we're not hand waving then. LLMs, abstraction removed, are deterministic computations of matrix-multiplication, f(x) -> y. If you want, we can make them pseudo-random, but thus still a deter
7.
by gopiandcode 5mo ago
It really depends on your model in my opinion. At the lowest level of abstraction, LLMs are just matrix multiplication. Deterministic functions of their inputs. Of course, we can argue on the details and specifics of how the peculiarities o
8.
by gopiandcode 5mo ago
As quoted in the article itself, please take it up with the chief architect of the Lean FRO: > ... converted zlib (a C compression library) to Lean, passed the test suite, and then proved that the code is correct. > Not tested. Prove
9.
by gopiandcode 5mo ago
Where are you coming up with this from? This is awfully confident for a fact you seem to have conjured up without evidence. As far as I am aware, Lean is interested in being used as a programming language (see: https://lean-lang.
10.
by gopiandcode 5mo ago
Yes, here's a concrete example: https://github.com/leanprover/SampCert This is an implementation of a verified sampler, in lean. Not an embedding in some other language. The implementation itself is in lean, and a
11.
by gopiandcode 5mo ago
Right, but what you're describing is a consensus protocol. It's called 2 phase commit. The point of the article is just that we should really be analysing these high level plans in terms of distributed algorithms terms, because th
12.
by gopiandcode 5mo ago
Lean-zip was not my project but one by others in the lean community. I'm not sure about the methodological details of their process - you might want to check with the original lean-zip authors ( https://github.com/kim-em
13.
by gopiandcode 5mo ago
It does seem that way doesn't it? But as software bugs are becoming easier to find and exploit, I'm expecting more and more people, including those not "sophisticated enough" to understand and employ formal verification
14.
by gopiandcode 5mo ago
Sorry, I'm not sure I follow. We are talking about bugs in a verified system, that is, in this case, a verified implementation of a zlib-based compression tool. Did it have bugs? yes. Several in fact. I'd recommend reading the art
15.
by gopiandcode 5mo ago
you can still verify arbitrarily long running programs - there are instances of such software, such as sel4 ( https://sel4.systems/ ) and certikos ( https://flint.cs.yale.edu/certikos/ ), you simply model
16.
by gopiandcode 5mo ago
Repeating myself, when we speak of bugs in a verified software system, I think it's fair to consider the entire binary a fair target. If a buffer overflow causes the system to be exploited and all your bitcoins to be stolen, I don&#x27
17.
by gopiandcode 5mo ago
Hi! Author here. When we speak of bugs in a verified software system, I think it's fair to consider the entire binary a fair target. If a buffer overflow causes the system to be exploited and all your bitcoins to be stolen, I don'
18.
Lean proved this program was correct; then I found a bug(kirancodes.me)
7 points by gopiandcode 5mo ago|0 comments
19.
Buffer Overflow in Lean_io_prim_handle_read(github.com)
2 points by gopiandcode 5mo ago|1 comments
20.
Multi-Agentic Software Development Is a Distributed Systems Problem(kirancodes.me)
1 points by gopiandcode 5mo ago|0 comments
21.
Vibe-Coding a Verified Compiler (JS-2-WASM)(docs.google.com)
3 points by gopiandcode 6mo ago|1 comments
22.
by gopiandcode 10mo ago
If it has become a cult, it's become a cult that has infiltrated so far as DARPA - see their TRACTOR program ( https://www.darpa.mil/research/programs/translating-all-c-to... ) I think couching the success and
23.
by gopiandcode 10mo ago
So to clarify, the crusade to rewrite things in Rust is not my fight. To be honest, I'm more a third party watching from the sidelines. There seems to be big institutional interest in replacing C with Rust. Not for ideological reasons.
24.
by gopiandcode 10mo ago
w.r.t the first point, so ideally you wouldn't want to do that because it'd incur a heavy runtime performance. Rust's memory analysis allows eliminating those kinds of memory bugs without having to check writes at runtime. w.
25.
Humanity is stained by C and no LLM can rewrite it in Rust(kirancodes.me)
3 points by gopiandcode 10mo ago|9 comments
26.
by gopiandcode 1y ago
oh yep, it's definitely more than usable for 'actual programming' beyond just maths proofs. Things like: - bindings to godot ( https://github.com/kiranandcode/lean4-godot ) - advent of code ( https:/&
27.
Why Lean 4 replaced OCaml as my Primary Language(kirancodes.me)
27 points by gopiandcode 1y ago|5 comments
28.
by gopiandcode 1y ago
Arguably it really depends on your DSL right? If it has a semantics that already lies close to existing programming languages, then I'd agree that a few examples might be sufficient, but what if your particular domain doesn't matc
29.
by gopiandcode 1y ago
Oh that's a great blog post and a very interesting point. Yep, I hadn't considered how LLMs would affect frameworks in existing languages, but it makes sense that there's a very similar effect of reinforcing the incumbents an
30.
by gopiandcode 1y ago
mhhm yes yes. There's a thread of discussion that I didn't quite chose to delve into in the post, but there is something interesting to be found in the observation that languages that are close to natural language (Python being fa

More ›