amoss

I'm on the Swedish list and I get exactly zero spam calls. As the parent post pointed out it is country specific.

Whether they are or not is irrelevant to the difference- there is still an explicit division between training and inference, with reinforcement of the statistics of the training set.

I think it is uncontentious that we are not designed at all. But to address the intended spirit of the question: are we restricted to output that is a close fit for our training set?

I would argue that we are not - because we do not have a rigid partition between training/test. Our ability to reason speculatively rests to some extent on ability to produce outputs that we have not seen before and which are statistically not like that which we have already seen. How we know which of these outputs to keep, and which to discard is (afaik) an open question.

The tu quoque argument doesn't really work here. LLMs are specifically designed to output either material from their training set or instances that look statistically like it. Humans are not.

If you are relying on live updates to change state in a dynamic language then you are not doing it "surgically", unless there is some other definition that means hitting it softly with a large rock.

Kind of weird how LoC has become a metric for people to chase again.

I don't think you can describe his beliefs using booleans like that: you have to use a numeric scale. It would be be correct to say: Elon would need a hell of a lot of ketamine to believe a colony on mars is a possibility.

Alternatively you may want to be a passive investor using the current rules for index inclusion, rather than having them altered to favor this loss-making trashcan on fire.

> The world seems to be fragmenting, into those that see the value in the latest from Google, and those that resist changes like this.

This reads as a strongly closed minded claim that has been "whitewashed into corporate appropriate speech" by an llm. If you cannot understand any validity to the other side of a debate then you are not engaging in discussion, no matter how your claims are dressed up.

That is the ugliest Ferrari I've ever seen.

kind of wild that you think there has been no shift in culture between 1970 and 2020

with a mastercard from a swedish bank that is the experience that i get. all online transactions pop up a page from my back with qr code, this is authenticated through an app that shows me the transaction details and requires pin confirmation.

Dead code elimination is run multiple times, including after other optimizations. So code that is not initially dead may become dead after propagating other information. Converting dead code into an error condition would make most generic code that is specialized for a particular context illegal.

Nobody said one rack. Your entire rant is misguided. He analyzed what it would take to put one rack on one starlink like package in order to build a constellation.

Later in the video he runs through the changes needed for 100kw per rack.

The details might bury his point rather than illustrate it. The driving theme throughout seems to be that a tool tuned for correct syntax, with deep understanding of semantics will look like a Dunning-Kruger machine. The specific errors that the author's colleague was oblivious to don't add any weight to that general point, they only explain one specific instance. It's classic omega-consistency.

feels like this comment could be shorter

Take it gently, the poor thing doesn't understand the difference between code and talking about code.

In addition both have a property similar to dispersion. In crypto each change to an input bit should cascade through as many output bits as possible. In ML each output bit should depend on as much of the input bits (and hidden layers) as possible. So they both feature a similar maximization of entropy.

> rollout will be incremental and it will self monitor by defining success conditions at rollout time.

This sounds a lot like allowing an LLM to define tests as well as implementation, and allowing the LLM to update the tests to make the code pass. Recently people have come to understand (again?) that testing and evaluation works better outside of the sandbox.

and then we start to embed comments

// concatenate pairs of parameters, e.g. x and y become xy

// the pairing of open and claw is vital to understanding the function

"in a wild or unsupervised state" seems like a particularly apt description of children. it does not seem to be derogatory: language really should be evocative as often as literal.

There are standard convex assumptions to handle incompleteness, decidability etc, i.e. the results are an over-approximation that terminates. Picking a approximation that is precise enough in the properties that you care about is part of the challenge, but it is an in-band problem. There are no hard edges between the theory and reality.

As with most engineering problems the out-of-band issues tend to be the hardest to solve. Models of the part underneath the interesting part need to be complete/accurate enough to make the results useful. Compare it to crypto where people do not usually try to break the scheme - they try to break the specific implementation of the scheme because the weakest points will be at the interface between the theoretical construction and the actual concrete instantiation of the device that it will run on.

The article describes fuzzing the library, this execution requires a program to be compiled. Typically fuzzing involves a minimal harness around the payload (a single call into the library in this case). There is clearly a bug in this program, and it does not exist in the minimal harness. It must be in the library code, which was covered by the proof.

The bounded, specific codebase that you refer to is typically the library *and all of its dependencies*, which in this case includes the Lean runtime. This is why formal verification is difficult: the proof chain needs to extend all the way down to the foundations. In this case the original gushing claim that everything was verified is incorrect and premature. The article seems like a good exposition of why.

What is the program?

There are two different answers to this question, and which one is "correct" depends entirely on the context of who is asking it.

1. It's the code that is specific to this program that sits above the run-time layer (internal view, that most programmers would take).

2. It's the code in the binary that is executed (external view, that most users would take).

The key question does not seem to be "was the proof correct", rather "did the proof cover everything in the program". The answer depends on whether you are looking at it from the perspective of a programmer, or a user. Given the overly strong framing that the article is responding to - highlighting the difference in this way does seem to be useful. The title is correct from the perspective that most users would take.

But is fair to state that the verification was *incomplete*, which is what the article does.

I would use this tool. Ship it

It's the old broken. Clearly it must be replaced with the new hotness.

Cybertrucks. Electric semis. Full self driving. Battery city.

I'll leave up to the reader to put them on the appropriate list.

I've watched Patrick's videos for enough years that I know he is not, but I still wonder from time to time. His voice is incredibly flat and uniform, he always uses fake backgrounds and there is extremely high use of jump cuts in his edits.