js8

Yes, you don't understand.

I have a schizoid brother. He never worked for a living his whole life (he's 46). He lives off my mum's income, and spends his day in front of the computer screen. He has no friends and no relationships.

Horrible, right? But he has a chemical engineering degree, and in his late 30s started to learn to cook. And, he (to the extent he's not addicted to the screen) helps my mum with chores.

So even he found a way to motivate himself to do something useful. And look, most people are not schizoid.

Under UBI, if you have some skill, you can get paid by people (possibly from their UBI) to do stuff they don't want to deal with. Many people will take that offer (to work more), just like many people pick more work, higher wage job over less work, lower wage.

It would be interesting to see if this new counting method has any implications to counting 2SAT or parity-counting of 2SAT. Since problem posed in XORSAT and 2SAT clauses is NP-complete, this could have implications about P vs NP.

> The companies were always trying to get coworkers together and have events (on company time) that got teams mixing and socializing across departments.

Really depends. These are people in the same social class. But I have never seen a cleaning lady that works as a contractor being invited to a corporate party event.

I don't think he believes in Antichrist, the same way Elon Musk doesn't believe we'll go to Mars. I think these are calculated statements to manipulate people. (The U.S. oligarchs find some of the more gullible fundamentalist evangelicans to be a useful ally.)

That being said, I think his straussian worldview is probably his own.

Why is everyone so hang on determinism? Monte Carlo methods are nondeterministic but still programming. We use random generators in many programs.

If I was brainwashed - maybe (hypnosis is sometimes called programming). But I am not, and AI agent is - it's trained to follow instructions, cannot help itself but do it.

Another difference is the binary code - I can run the same agent on a different computing substrate (e.g. different CPU), but with humans no one can do that. That has implications, we can study or modify AI agent behavior, for instance.

Some compilers can do that, but only in a very controlled way. For example Haskell's deriving or inference of the correct method called on typeclass. Or the Prolog/Datalog/SQL - they will also fill in many details on how to arrive at an answer.

I think this might be a false dichotomy, because for instance, I think LLMs are programmable in natural language, and they act as compilers, I even think they can replace programmers; but still I agree with Dijkstra, that programming in natural language is a bad idea.

But I am going in an opposite direction. Instead of rejecting formal languages in favor of natural ones, I think we should embrace formalism even on the level of specifications, requirements and our model of the world. Partly because that's what LLMs actually do - they de facto formalize these things.

Claude also checks well-formedness - if you give it gibberish instructions, it will respond that it is gibberish and do nothing.

On the other hand, there exist programming languages (like Jot, a certain encoding of combinatory logic) where every binary string is a valid program.

Of course instructing agent is programming; the agent is an interpreter (albeit in some cases nondeterministic, but that's true for most programming languages that have a function to get current time) of the natural language. How exactly it is interpreted is given by the weights, the context, and possibly the random seed.

But even if we write in Python like foo.bar(), the interpretation depends on what is in module foo and function bar, how they are defined contextually.

You can try to find some difference but most modern AI agents come more close to a language interpreter than not, if the actual instructions are given.

OTOH, giving instructions to people is not programming. People do not consist of binary code that is reliably executed; they are biological organisms subject to environmental pressures such as being tired. They have their own consciousness and will, and can refuse to follow the instructions. LLMs are programs; they cannot decide not to respond.

I don't think this is a productive discussion, I tried to make my point clearly, and never said anything about beaches.

At the end of the day, the program was asked for by somebody, and that person described what they wanted. Whatever the program does, it can only be as much correct as much unambiguous was the description that conceived it.

The description was most likely given in a natural language, with many assumptions about the shared objective reality.

Today, we have LLMs, which de facto (but with significant flaws) formalize the interpretation of natural language, as well as the shared objective reality we inhabit. They are becoming closer to the truth than any individual human. (Their construction is a wittgensteinian program of sorts.)

So we can take an LLM with the prompt "Respond according to the following specification:" plus the original specification/requirement, in natural language, itself, as a program A.

Then we can take the written program itself, together with the emulator of the machine it runs on, as a program B.

We can feed both of these into some theorem prover - and formally prove that program A and program B give identical outputs on identical inputs. That's most likely the best we can do, ever.

(Or we can, in theory, develop programs this way, as a solution to the following question: Which program, when run on the given platform, gives provably identical answers to program A? That's a general program synthesis problem.)

If you're able to detect where you use these hard-to-analyse functions, then yes. This is feasible on source level, and maybe known compiler binary level. I think ultimately people will want to validate properties of binary code against the model specification of their hardware.

Although the prover might be smart enough to say, "this function is getting kinda complicated, let me model it as a random variable and see if it's enough". I think LLMs can kinda do it but not sure if your typical theorem provers can (it's on the level of being able to employ probabilistic proof techniques).

Actually, bugs might surface during such restructuring. If the statement you're proving can be greatly simplified to something reasonable, if we omit this one weird special case, that indicates a bug in the specification.

While I completely agree with 3uru, where it can get stuck is if your system contains a pseudorandom generator or some other cryptographic shenanigans. These are programs deliberately made difficult to analyze and reason about.

I would say, in practice, you are more likely to encounter complexity barrier (we don't know how to decide some NP-hard problem fast enough) to proving things about your program than you're to encounter a true undecidability barrier (Rice theorem).

Except COBOL systems are often easier to formally verify than modern systems.

They're often simpler, and whole classes of security vulnerabilities are mitigated by design. My favorite example is SQL injection mitigated by having proper access controls in the DB. Why prove about every SQL statement that it cannot be nefarious, when we can just prove it about the connecting user? The user access carries the intent of what the application program wants to do with the database, in a separate channel, independently of the complexity of the application.

The ecosystem migration (usually to higher latitudes) due to climate change is quite well-documented. And you want to do it back and forth?

I am not saying I have all the answers, I am just not convinced that "returning" is strictly better option.

I agree, I believe I would disagree with most of the Hammurabi's code, and I also happen to disagree with the majority of the ten commandments. (I am an atheist leftist humanist, cosmopolitan liberal socialist.)

> while having way less diversity of answers to that question than humans would

Isn't that to be somewhat expected due to https://en.wikipedia.org/wiki/Aumann%27s_agreement_theorem ?

"Going back to 1.5 actually means less damage than not going back."

That's a different claim, but also no. Let's imagine we go 1.5 -> 2 -> 1.5 in a few decades (and keep in mind capture is more difficult, so the 2nd transition will take longer), compared to just 1.5 -> 2. In the return case, we stress all the ecosystems twice by change, rather than once. So it's not at all clear it's less damaging.

Large enough context window is enough. Yes, the md files can be filled back in, but other stuff (unneeded details) can be swapped out.

Yes, but we are really talking about LRMs not LLMs. They can emulate working memory so well that many people even recommend using bunch of .md files (as a sort of out-of-context notes) instead of RAG based on vector DBs. They can maintain context, by compressing it and writing out memories quite autonomously.

So yes, even though not updating their weights, they can learn plenty new things and concepts, and build new models of the world.

It was suggested by TFA:

"The urgent task is to ensure that global warming remains below the 2°C threshold, with the aim of returning to 1.5°C by the end of the century."

I disagree it's impossible but I agree it is difficult, and (as I said) the damage will be done.

I am not sure you're correct. Yes, from the physical perspective of LLMs design, the above is correct. But they are also systems that evolved to do things through training; so you cannot discount the possibility they can emulate building of new abstractions in another level.

LLMs already have the concept of "reference" - i.e. I can say a name of something, for example of a function, and they understand that the properties associated with the name itself are not relevant, but rather whatever the name does refer to.

But this is pretty much what you need to build new abstractions. You need to name a paragraph with the definition (explanation) of a concept, and be able to recall the paragraph by the name in order to do inference.

So with references, they can get around the context size limitations, like humans can. It's slower than learning things "by heart", but I think LLMs are perfectly capable of that; and the evidence is, they are able to navigate codebases larger than their context, which often contain many new abstractions.

I disagree. LLMs might create incoherence not because of context size limit is too low, but because it's too high. The limit is vastly higher than for humans.

But to overcome the limit, one needs to adopt simpler, more coherent models of reality, which is what I believe humans do. But there is little motivation to do so if your context window allows you to understand the situation in full.

So it seems there is a tradeoff. Some solutions (proofs of complicated statements) might require context of certain minimal size. So human solution doesn't scale.

Maybe we should try to adapt the context window to the system being worked on, to ensure that the system architecture has the structure viable in the minimal context size required.

That's not what I am saying at all, I am just pointing out that venturing to 2 degrees (or more) and back to 1.5 degrees incurs the cost. Maybe it's well-known at this point, and I am just stating the obvious; but it's not my general impression.

Unfortunately, even if we exceed and then bring temperature back to 1.5 degree over preindustrial, the damage has already been done. Many ecosystems and species will be lost, and many of the feedbacks (for example arctic sea ice) have hysteresis in them which will not get us to the same state even though nominally our temperature will be lower again. And because of hysteresis, larger reduction in CO2 might be required to get us back to 1.5 degrees.

That's why all this CO2 capture and drawdown using some kind of unspecified, new technology, is such a distraction. Ideally we shouldn't release the carbon in the first place.

As much as I wish 2027 to be the year of Linux Desktop, I'm afraid the companies will just "up the ante" by making all the APIs and boundaries much more convoluted, with AI watchdogs and remote servers along the way.

How can people today even think they can "move to the U.S. permanently"? U.S. is even considering stripping citizenship from its own citizens. It's very impermanent.

I phrased your view differently in my earlier comments - we already allow "nondeterminism" (or better call it chaotic behavior) in compilers. But usually it is only limited to performance (CPU and memory consumption).

So the "LLMs are chaotic" (difficult to predict) argument is somewhat moot; the performance of GC language runtime or even modern CPU with hyperthreading is already chaotic too.

I think for many applications, people will treat correctness the same way.