Viewing profile — gopiandcode

> 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) ( '(1,2,3) ```…

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 …

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

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…

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

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

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…

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…

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

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? y…

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/certi…

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

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

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

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…

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 …