Some important background for this is that, around 1900, mathematics got formalized to the point that there is a standard for whether a proof is valid or not that doesn't depend on humans thinking about it, just doing a bit calculation following an algorithm. However, it is such a large calculation that nobody wrote complete formal proofs or verified all of the steps (since they'd be spending huge amounts of time on obvious parts, and not the novel aspects). Then, in the past 20 years, people have made computer systems that work on complete formal proofs while showing you the interesting parts, with the rest in macros, and check these proofs automatically. This means that finding proofs has the form of things like what AlphaZero is good at: something to check if moves are legal and a win condition. However, only a relatively small portion of mathematical research has been put into Lean so far, and that doesn't include the sorts of obscure results that often turn out to be useful in other problems. So the current wave is using LLMs to find results in the literature that might be relevant and producing formal versions of them, game AI to put them together, and deterministic validation to check each of these as it goes along and then people can see at the end that the calculation shows the proof is valid. The only part requiring mathematicians is checking that what the proof proves is what they understood the open question to be.

Adoption is a function of existing adoption and existing availability of resources.

Extremely good OS' and truly amazing computers have failed, not because they were too expensive or had issues, but because they were perceived to be unpopular OR simply lacked enough software that could run on them.

Extremely bad OS' and truly awful computers have succeeded for the opposite reason.

Linux has an extremely good architecture, at least for machines that are mostly operating with CPUs. When most of the work is done by the GPU, it's less obvious that Linux provides the necessary mechanisms to manage resources and abstract away the hardware specifics. That doesn't mean I expect Linux to start fading, but I don't think a centralised OS is necessarily where things will go. However, the reason it hasn't done better so far is simply because potential users and potential software houses had a negative view of it (even though actual users were almost invariably loving the system).

Windows is crashing now not because it is a slow, bug-ridden piece of spyware (which it is, but users have never cared about that in the past), but because it is perceived in increasingly negative light.

They can get vertical samples from space and the ground. What they can't get from space or the ground is how the internals of a system evolve.

The problem with "models" in the abstract is that there are a lot of them and some of the time the thing you want is to know the same point relative to the system and not to the mudball.

Lots of people have gut feelings about AI, positive or negative.

Most of the AI research I can see people doing is focusing on single-element problems (such as finding counter-examples to a mathematics hypothesis) or solving very simple engineering systems (at most a dozen or so components). Most of the benchmarks are even simpler (write a short story at the level generally asked in English classes of primary school kids).

As a result, I think that people have developed either a very cynical outlook or a very optimistic look. Neither of these is entirely realistic, for the simple reason that no actual useful problem fits any of those descriptions.

Digging much deeper, I'm finding that when problems get into the hundreds or thousands of elements, even ChatGPT Sol 5.6 and Claude Fable 5 struggle badly to keep track of accurate relationships, let alone any level of detail.

If you want to solve a relatively simple coupled system (whether to use solar panels or direct solar heating, and which side of the house to place them), I'm sure AI is fine. If you want AI to write a five hundred word story detailing a conversation between Kim Possible, Rufus, and a smoked herring, I'm sure it could cope. Just.

If you want it to do anything hard enough that a human could do with an assistant, the tests I've been using (meaningful rather than synthetic problems) suggest you've developed a fantastically expensive blue smoke generator. We are going to need to see the inference engines developed for previous generations of AI, and the reasoners developed for the semantic web, and perhaps tools that haven't begun to be imagined yet, before AI can do anything non-trivial.

A balloon is not static, it moves with the atmospheric system it is in. Ergo, it tells you how that system evolves. A drone cannot do this.

A drone can stay put, relative to the ground, telling you how a location's atmosphere evolves. A balloon cannot do this.

These are solving completely different types of problem.

You could, of course, construct a hybrid, as balloons are traditionally single-shot. If a balloon carries the measurement gear and a drone capable of carrying that same gear PLUS a deflated balloon, then you can have something that operates as a balloon until it reaches some pre-set location, whereupon the balloon's gas is released and the drone flies the ensemble to a collection point.

So....
- add a new AI feature that has no purpose other than misinformation and abuse
- roll back release of new AI feature as soon as completely predictable misinformation and abuse occurs

What was the point of this?

It obviously gives us guarantees in terms of what the source will do and what the compiled code should need.

These do not provide memory safety, so memory bugs would not be solved by these. They will find unexpected behavioural issues, though.

The precondition and postcondition statements are not cunningly-disguised assert statements because they're not asserted at runtime. They're enforced at static check and/or compile time.

The policy hints mean that if the kernel is doing something you're not expecting, you find this when testing the code. Equally, though, it means that users cannot cause the software to venture into realms unknown through many of the usual attack vectors because those will require permissions that aren't there.

tldr but the two examples are pretty dumb as anyone in those fields could doubtless figure it out. If you give a model sufficient data, even if it is just axioms, understanding of basic physics and chemistry, has holes, etc., it will be able to fill in the gaps or tell itself a story or roundabout logic walk that gets there if possible. As far as not being able to tell where instructions come from, the rules they try to implement are flimsy and less grounded than the massively interconnected data they have. You would have to not tell them about the concepts of drugs, poison, sabotage, aircraft, etc. and not let anyone tell them about it. It just isn't feasible. Humans have even less internal security, which is why media brainwashing works. In fact you can get incensed about something that is fake and even after looking up to see if it was real or not, still be upset about the hypothetical situation. And people can love AI created "animal came to my door looking for help saving its mom" videos, even if they know it's AI generated the response is "I don't care, it's so cute!" It's also why willingful suspension of disbelieve and works of fiction sell. I do have an idea about a solution (not enough space to write in the margin here, lol) but it is not going to depend on a single LLM policing itself within the turn.

What the hell is that? Is that a salesman in PC-speak?

TFA would be unlikely in a sci-fi world. The Perry Rhodan series which was widely criticized for fascism at the time, so really not a great example given today. I'm just talking about the supertechnology side of it, runaway galactic fueled engineering feats. Maybe someone knows some better novels with data centers and mass-scale construction projects, robots, etc.. Iron Man is too hand-wavy though some guy did make a Jarvis.. Well even though I only read the first 100 episodes that were in English, Google AI overview has read all of them (German mainly) it seems. It confirms there are tons of robotic data centers in there, who knew?

Anyway in the a super sci-fi world, humanoid robots or some kind of robotic components and AI controlled designs would be state of the art, everything else hopelessly outdated. The data centers would be built to a common layout and robots would be used. Power? Yeah, fusion but whatever, it would not be overloading our grids and water supplies. New robotic powerplants would be built at their core. Things would generally not be built to human scale, just the control rooms would be. Anyway the point being, it would all be engineered. Yes there are electricians in the future too, but they are probably not building data centers but small spaceships, Scotty's got an EE degree or 10, etc.

So is the ridiculously bubbly money we see now just being pumped into outdated frameworks such that a lack of human electricians will stall it? It seems laughable. These guys are not playing to win, it just sounds like dumping money into a financial supply chain without actually say, trying to design and build the most efficient, large scale data centers leveraging robots and AI.

Instead, it just pumps money into a chaotic sump and random companies end up wildcatting this without regard for local water and power grids. How about making a mega version of those concrete house building robots, laying fiber with robots, putting wind, solar and gravity batteries all over it? I guess it is too much to hope that anything tangibly useful could be created from all this money before it goes poof..

I got Google Play Music for my family back when that was a thing. It was the same price as Spotify, had the same catalog, and included any music on Youtube as well. The fact that it included ad free Youtube was just a bonus. These days that has morphed into Youtube Premium, and I still pay for it. I am mostly there for the music, but the ad free Youtube is not terrible.

The interesting thing is that it is pretty clear that most people just watch the ads. Youtube had $60 billion in yearly revenue last year. More than Disney, NBCUniversal, Paramount, and Warner Brothers combined. Roughly $20 billion of that is credited to Youtube Premium which is bigger than any of its Hollywood competitors.

There's a reason that Peacock is being included with Youtube Premium and not the other way around. Youtube is worth something. Peacock, not so much.

Things have changed dramatically since the heyday when everyone had a cable subscription. I used to work for SlingTV (and then Dish), and I had a front row seat as the whole industry imploded. Every year the television networks and movie studios would sit down and renegotiate their contracts. Despite the fact that viewership was always down at least 10% year over year they always wanted price increases. If the cable providers pushed back (as Dish often did) they would lose access to channels, invariably during football season when it mattered most.

You see, as technology started allowing people to purchase their entertainment piecemeal it soon became clear what parts they were willing to pay for, and which parts they weren't willing to pay for. Hollywood thought that people paid for cable subscriptions to watch their scripted television. It turns out that, for most people anyway, the part of television that they were willing to pay for was live sports.

That's why Disney won't sell you ESPN unless you bundle it with everything else that they sell, and that's also why Disney is suing SlingTV for reselling access on a daily basis. SlingTV's "sports pass" allows you to pay for just the games that you want at a ridiculous price. Disney should be stoked, but instead it has sued because it wants to force sports fans to continue to pay for their other channels.

Almost no one is watching traditional scripted television these days. The few hits that the networks do have tends to be reality TV stuff like "Dancing with the Stars," where the audience can watch people compete in real time. Youtube (not YoutubeTV) has at least half again as many viewers as their next highest competitor (Netflix), at any time during the day, on traditional 10 foot devices (your living room TV). That's not counting people watching Youtube on their phones or their computers. Youtube is killing scripted content on living room televisions, during prime time. During the day its an order of magnitude worse.

Take a look at nielsen.com and take a look for yourself. It's absolutely grim. Look at the shows that are doing relatively well, they are all either sports or sports commentary. That's literally the only reason that anyone watches anything besides YouTube and Netflix.

Apple spent over $20 billion building up a content catalog. At their height they were spending nearly $5 billion a year making shows. They made some great shows and got rave reviews. Amazon spends $1 billion a year for the rights to Thursday night football. That is arguably the worst football game of the week. However, Prime generally gets as many viewers for a single game as Apple has total subscribers, including all of the free subscriptions that Apple gives away. It's not just Apple that is shifting away from scripted television either. Take a look at any of the streaming sites (including Netflix) and you will see that all of their recent moves have been to try and compete for the sports market. That's definitely what YouTube is doing by bundling Peacock.

Hollywood is currently circling the drain. Everyone is up for sale right now. No one is watching scripted television. They certainly aren't paying for it.

His podcast Better Offline is squarely targeted at people who are very much online. Indeed his entire gig is the epitome of online living.

If Ed Zitron really felt better offline, he wouldn't be making a living off of a podcast and constant AI bashing.

Not that I necessarily disagree with him though... It's just that the messenger doesn't really befit the message.