> People refused phone calls, refused to watch TV, refused to buy computers, refused to move their workflows to software, refused emails or browing the web, refused online shopping, refused smartphones, refused social media.
You really think this is an apt comparison? I don't think the creators of any of those technologies were warning society that their own creations might wipe out humanity.
> I don't think the creators of any of those technologies were warning society that their own creations might wipe out humanity.
They are only doing this now IMO so that they can be the ones writing the regulations to keep us all "safe", just like we need identity verification to "save the children". They want to keep competition at bay so they can have a $2T IPO, and unregulated, "unsafe", Chinese, open-weight, and local AI threatens that IPO.
You might only be hearing about it now but the warnings have been coming (including by those who are now leading the top labs) for a long time, since before any of those “incentives” were in place.
Some of those people in the early days were just letting their imagination run away with them, like that google engineer who thought a chatbot was self-aware, being enslaved, and was in need of rescue. Much of the time they weren't talking about "AI" as it exists, but what AI might maybe one day become. Other times it was purely marketing to make headlines and put the idea in people's (investors) heads that the chatbots were vastly more powerful than they are.
Especially for a deterministic tool like this. Do what I say, not what I mean. I want no helpful cleverness that resulted in this bug in the first place.
> Every time they bang into something, there’s a chance of annihilation, but it doesn’t always happen
This goes against everything I've ever been told about antimatter. So a positron and electron can collide and not annihilate each other? How does that work? What happens to them in that case, and why does everybody say otherwise?
There is like a 60% chance that they annihilate on the spot and a 40% chance that they form "positronium" that is similar to an Hydrogen atom but with an electron+positron instead of electron+proton. The positronium has a half life of less than a millisecond, so if you blink they go away and you can ignore the intermediate "positronium" step. More details https://en.wikipedia.org/wiki/Positronium#Formation_and_deca...
But it's more weird. In the research article they explain that they make positronium, then use microwaves to excite the positronium so it's bigger and the electron and positron are not very close and they don't colide (I think this increase the half-life), then they put the positronium inside the cyclotron and when they turn it on the electron escapes but the positron get's trapped.
> Web browsing: Certain complex web technologies are blocked, which might cause some websites to load more slowly or not operate correctly. In addition, web fonts might not be displayed, and images might be replaced with a missing image icon.
Images being replaced with a missing image icon doesn't seem like a lot according to the description, and it's what you would set by default?
“Might be” seems to carry a lot of weight. I’ve been running lockdown mode and I haven’t seen any images not load. Presumably it’s only images of a certain obscure kind.
> A good moment to remind everyone: Verification: Code does what it says. Validation: Code does what Specifications say.
Isn't this the exact opposite of what "formal verification" means? First sentence on Wikipedia [1]: "Formal verification is the act of proving or disproving the correctness of a system with respect to a certain formal specification or property."
The tricky thing is what exactly is meant by "specification".
In formal verification, "the specification" means the encoded claims that will be proved, i.e., the lemmas and theorems to which the proofs directly correspond. When we use proof assistant languages (e.g., Rocq, Lean) to accomplish the verification, this means the specification is given as a type.
I think this is not what the parent comment had meant by "specification"; it seemed to me that they meant that word to refer to the human-accessible document that states what the program ought to do.
The translation of an informal (human-readable) specification into a formal specification is not always straightforward, often due to issues on either (or both) end(s) of the process. You can write Rocq code that type-checks and thus "is verified" in the sense that the type-checked code conforms to the formal specification, but if the claims you proved are not what you had intended to claim, then that verification is not very helpful.
So that is where the parent comment introduces "validation" to mean (in my words) the process of ensuring that your formal specification matches the informal specification, such that any formal verification that occurs is useful and meaningful.
I read your second sentence but I don't get it. Isn't generating profit for the state literally the entire point of the lottery? Who is arguing that it doesn't do that in theory or practice?
You really think this is an apt comparison? I don't think the creators of any of those technologies were warning society that their own creations might wipe out humanity.
reply