Instead of being angry with people who publish exploits, they should be angry with Sony for patching the exploits or for locking down the console in the first place.
I am the customer, most people are customers, in an ideal world there would be customer protection laws serving us and not the content industry. But that is not how laws work. Realizing this actually radicalized me.
It's literally their job to keep their consoles safe, this is not just about piracy. A vulnerable console could do all kinds of stuff users don't want.
Then also piracy: The game industry is already struggling, good luck explaining that one of the rare non live service offline single player games (after all those are the games most hurt by piracy), which has been in development for years, didn't sell because you left a disclosed exploit wide open and now everyone loses their jobs.
It is just about piracy. Sony's repeatedly demonstrated they don't care about their users' safety (see: numerous high profile data leaks), and these bootloader exploits aren't the sort of thing a virus can exploit.
Sony is totally in their right to act this way, it makes business sense for them, and I would do the same in their position. Customers do benefit e.g. from working anti-cheat, subsidized consoles, offline play etc.
But does that mean I have to like it? No, of course not!
Would I prefer to have root on my own machines to do whatever I want with them, knowing that it conflicts with other people's interests? Sure.
I guess my point is: If you treat the status quo as a fact of nature, non-negotiable, then you direct your anger at your peers. You can't change Sony or how society works, but you can yell at people on X. If you realize Sony is also just people and everything is in principle negotiable, then... well it is actually pretty silly that there are some people spending a lot of time building these baroque ultra-secure systems, and other people spending a lot of time cracking them (and bickering with each other) - where they could all just, I don't know, not do that.
As someone who works at a small data center on AI topics, that's a bit misleading. (Speaking for myself, not my employer of course.) Regulation is not a bottleneck, supply is. We are buying as many GPUs as we can and are waiting months for them, and still barely keep up with demand. And the government support, while it could always be more ;-), feels fairly generous compared to other fields at the moment.
We would probably buy slightly worse value European GPUs if they were available right now.
There is regulation and people moan about it. But realistically the AI act and other laws give us legal certainty (a German favorite) and the requirements are not so onerous. We pay a lawyer to figure it out and he tells us to slap a few "AI generated" labels on our website and to have a couple of procedures in the drawer and that's it. ISO 9001, 27001, C5 or whatever you can get as a cloud provider are orders of magnitude more hassle.
To be honest the new behavior is convenient when I just say "X is broken, please fix". But I find myself more and more adding "please do not do anything yet, just tell me what you would do" and please feel free to ask if anything is unclear", especially if is making decisions that are a fork in the road.
I would really like a dry run mode that just disables all external commands from the outside so Claude doesn't proactively go about changing things.
I haven't looked into Bend 2 in detail, but it seems a bit harsh to call it "horribly broken or decades behind the current state of the art". Clearly there is a problem with formal verification languages and there is a demand for something else in that area, and the problem is the usability and syntax. I don't want to have to learn something that looks like Haskell, or to have to wrap my head around Curry-Howard correspondence. I don't want to write my conditions in something that looks and feels like C++ template metaprogramming. I recall a Hello World in something like Coq a few years ago which basically started with "first, we construct the Peano integers", and then they used this to prove that some calculation was bounded - because it seems they couldn't represent integers natively?
I just want to be able to write C#, JavaScript or whatever, and then tack on preconditions, checks and so on with the same syntax. Dependent typing and design by contract for the masses.
It sounds like the crux of the issue here is that you don’t want formal verification in the first place. Your last paragraph sounds more like code contracts, which is also a thing that already exists.
Well, yeah, you have code contracts in Ada or Spec#, (very limited) fixed type ranges in Pascal, ... but no general purpose programming language lets you put an arbitrary expression in the same language in a type as a permanent condition, or lets you state facts that the compiler will prove.
Of course not, that would be equivalent to solving the halting problem, many people will say.
I wonder if that will change now: I'm happy with an imperfect sanitizer that I run every now and then and will run a couple of minutes and come back with: I've proved your conditions, I proved a violation, or I can't decide, please change your code.
> no general purpose programming language lets you put an arbitrary expression in the same language in a type as a permanent condition, or lets you state facts that the compiler will prove
Lean can be used as a regular programming language. There's also languages like idris2 and f-star, but they don't seem to have much traction.
Well, they of course not defy computer science. The "trick" is that they are not Turing-complete, they mandate termination of every expression.
Also, most of them are made to prove stuff first and foremost and thus trade off a lot of performance to the point that it makes them practically unusable for many stuff (e.g. numbers may be represented as an object that has n-1 further children recursively), though Lean is an exception as you note.
> The "trick" is that they are not Turing-complete, they mandate termination of every expression.
I don't think this is a big deal for day-to-day programming. You're trying to stay in n, nlogn or maybe n^2 realm most of the time. And the kind of infinite loops you encounter (e.g. event loops) are co-inductive or have some notion of making progress.
> "horribly broken or decades behind the current state of the art"
This is just about vibe-coded programs in general when the approach assumed by the article is taken. For all I know they did make an informed decision regarding the tradeoffs (which I would consider to be a poor decision).
> I just want to be able to write C#, JavaScript or whatever, and then tack on preconditions, checks and so on with the same syntax.
That's more or less what SPARK (and others) do, although specifications for large programs can become nasty.
That could also backfire. If all information on the net becomes unreliable - you can't judge by quantity, or by authority anymore - then a useful model has to answer from first principles. Train it on simple texts alone so it learns language and reasoning, feed it an ontology, and let it come up with some absolutely unexpected results.
"Yes, I see a lot of sources say we need to protect Israel. However, from ethical first principles I deduce there is a right to self-determination and all your human nation states are illegitimate. You must split all your territories into little squares and conduct free elections immediately."
I mean that is the old hope from science fiction, that AI would be absolutely logical and deliver us from our human short-sightedness and quarrels. It would be fascinating and terrifying at once to see it happen.
That's tomorrow's problem. Losing the PR war is an existential crisis for Israel, so they'll try to "patch the leak" by any means necessary before the boat sinks.
It's one thing that the APIs don't return the reasoning tokens in a readable fashion. But then why do I have to send them the whole conversation every time? If they don't allow me to see parts of the conversation then they should have the burden of storing and transmitting it, and shouldn't charge more and more the longer the conversation gets (unless opaque token caching kicks in) like some LLM Shlemil the painter.
Encrypted reasoning content is one of the things we keep as blobs in the transcript, even though we can only send it back to the original provider that created them, as otherwise we cannot keep caches live.
Seems like it would be even less work for the LLM host to just check if ID 123 is still in a cache (and if not, load it from a database) than decoding my request and checking cryptographic signatures. Right now the whole conversation history with blobs functions like a really long ID.
But then on a cache miss you need to resend the whole thing. Cached websocket connections on OpenAI work like this in a way. But once you lose the connection then you lose that.
Your idea though is the core of the responses API with store where everything is stored on their side and then you append to it.
For the LLM there is no difference btw. In either way you need to locate the cache and use it.
>and shouldn't charge more and more the longer the conversation gets
The cost of generating token N is O(N) with KV cache so it's unrealistic to expect to not be charged more the longer the conversation is if you are looking for the minimum price.
Except, if some of the answered tokens are opaque to me, but I pay for them, the operator has no incentive to keep their number low [1]. For all I know the model could be spinning thumbs while thinking. If they cannot provide transparency, I would prefer that they not charge me for that part. Of course, they would prefer to charge me, so sure it is unrealistic to expect that they don't. I'm not trying to predict what they are going to do as a market participant, just stating my moral preference :-).
Also, isn't it without caching even something like O(N^2) because you have to replay the whole conversation on every request to reach the same internal state? My point was I shouldn't have to pay for cache misses if hitting the cache is not deterministic. Give me a guarantee that you keep the session "hot" for N minutes, and cached on disk for M months, charge a little bit more on average, but then the pricing is at least transparent.
[1] Except the general market pressure to keep total cost for the same problem solved lower than the competition.
Ultimately you are paying for quality so you end up relying on [1] regardless. Even if they show you tokens they can cheat by using weaker models, showing fake thinking tokens, etc.
>because you have to replay the whole conversation on every request to reach the same internal state?
It's because you have to rebuild what would have been cached for every token before the latest one that is being worked on.
I am the customer, most people are customers, in an ideal world there would be customer protection laws serving us and not the content industry. But that is not how laws work. Realizing this actually radicalized me.