cobbal

All great questions. You're dancing around the edge of model theory here and the difference between truth and provability. It's probably past what can be explained well in a comment. Nevertheless, with omissions, simplifications, and my limited knowledge:

In logic, a model is a "set" of objects and all the true facts about those objects. For example, the integers and "1+1=2,1+2=3...". If a model deals with truth, then a "theory" is a mathematical structure that deals with provability. For example, the theory of groups contains an axiom "a+0=a" that applies to any a.

We say that a model "models" a theory when everything the theory proves is true in the model. The integers are a model of a group.

But, the integers mod 2 ({0,1}) are also a model of a group, but a very different one.

So, consider the statement "1+1≠0". The theory of groups isn't powerful enough to prove or disprove this proposition. It is a false statement in the integers, but a true statement of the mod2 integers. So there is a gap between what is true in a model, and what is provable in a theory.

(Look up both godel's completeness theorem and his incompleteness theorem for more insight into this relationship)

Back to turing machines, our most popular foundations of math is a theory named ZFC. With this theory we can prove many things, but there are also many things that can't be proven or disproven. ZFC lets us prove that "BB(500) is an integer greater than 5". But it doesn't let us prove that "BB(500)=174936...35" (pretend that's a concrete number). In fact, there probably is a model of ZFC where it is true that BB(500)=174936...35, and there is also probably a model of ZFC where BB(500)=284729...86.

Axioms define what is provable, but godel showed that there will always be more true things than there are provable things (if your theory is finite-ish). Most concrete questions about the BB function will never be provable.

As others have said, the sequence is infinite, though unknowable. Even if math can't say what the precise value is, it can still prove things about the shape of the sequence.

As a simple example, we know that BB(1000) <= BB(1001) (since you can encode the longest running 1000-TM with an extra, unused state as a 1001-TM) even though we will never know either of those values.

The argument that it grows faster than any computable function is similar in that it proves things without knowing concrete numbers. (I'd have to look up the details of the proof to say more)

That's correct. In particular, k=8000 is enough (probably much lower)

https://scottaaronson.blog/?p=2725

I review code line by line and build a mental model of the software as I review it. I find plenty of important bugs that way. PRs are an opportunity to learn (both committer and reviewer), communicate, and improve the quality of code a team ships. Sadly, many people decline that opportunity for the sake of short-term velocity.

If those systems are changing the semantics, they are buggy. If an LLM is changing the semantics, it's a tuesday.

Finally we've built the reverse centaur from Cory Doctorow's classic novel "Don't Become the Reverse Centaur"

Why is it unrealistic? We have decades that prove people can make games without AI. Is the unrealistic part just expecting people to be honest about whether they used it or not? We somehow manage to have the food industry mostly honest about what they put in.

I am now imagining a future where developers buy fancy "grep cards" for their machines. I don't hate it.

Twitter promised an open publishing platform with extensive API access. They're the ones who broke the (social) contract, not us.

This is definitely true in an information theory sense: having more knowledge is always better than less knowledge. However, it may not be true in math as a social human endeavor, and having answers without interesting paths to get there may not expand human mathematics in the same way.

If Fermat had a book with larger margins, would Weil have devoted so much time to proving the Taniyama-Shimura conjecture? No one can say.

It does sound totally ridiculous. Sadly it may not be. Previously discussed: https://news.ycombinator.com/item?id=48956688 "LG monitors silently install software through Windows Update without consent".

You can argue if it actually installs the software or just nags the user to install it, but neither are things microsoft would allow a monitor "driver" to do if they had any integrity.

Lost me at the first assumption. People can argue about how useful AI is, but it's obviously not essential because we somehow managed to write code without it a few years ago. I would even say the code was better back then.

The two tasks of writing code and engineering software cannot be separated without damaging the integrity of the mental model of the engineer. Having architects who didn't interact with the code always produced map/territory mismatches.

AI is a technology for removing nines from uptime, and adding them to Sturgeon's law.

ACM agrees I think: https://dl.acm.org/openaccess

> Beginning January 2026, all ACM publications and related artifacts in the ACM Digital Library will be made open access.

Determinism isn't the main hurdle. It would be a moderate effort to engineer a deterministic claude that would be no more useful than the current one.

The key characteristic of a compiler is that it takes a source language with a well-defined meaning to a target language with a well-defined meaning.

The reason claude fails to be a compiler is that its input language (english) can't be precisely defined. (And even if that were possible, it would very often fail to preserve the meaning when "compiling")

You may have been thinking of this one instead https://what-if.xkcd.com/141/ . Maybe we should put Randall on the supervillain watchlist.

This is a case of lethal trifecta. This particular one can be fixed by either not giving the AI private data, or by removing the exfiltration opportunity. Why does the comment-summary bot need access to your private video ids? Why does it need to be able to output links?

Most cases of prompt injection are harder to fix, and the success of the products they occur in relies on engineers who should know better sticking their heads in the sand about security risks.

Sadly, I suspect this will be the best piece of marketing they could ever hope for. "It's so advanced the government made us add extra security* to stop hackers!"

*(ask it in a more stern voice)

Here's the threat model I (a luddite) use to evaluate these. The claude code harness can be mostly trusted, the model cannot be trusted because it is exposed to untrusted data from the internet, and there is no separation of data/code in an llm [0][1].

I want to avoid running untrusted code on my local machine, because it could steal secrets, install malware, etc.

Since the model is allowed to write without restriction (I think) to the project directory, anything in the project directory is also untrusted. Running standard commands from the system is fine, as long as you know what those commands are going to do. Running anything from the local directory should be avoided because the code is untrusted.

This is just one security model, there are many others! If a person is running claude in a stronger sandbox, that changes the model considerably. What threat model do you use to evaluate whether an agent's actions are safe?

[0]: https://www.schneier.com/essays/archives/2024/05/llms-data-c... [1]: https://simonwillison.net/2025/Jun/16/the-lethal-trifecta/

That's funny. It told me that blocking "npm run build" was the wrong answer. Maybe it doesn't really under The threat model.

If co-authorship implies holding rights, then what gives the "primary author" who just prompted for the code the right to add their own name?

It makes up for that by also multiplying the productivity and happiness of the people who have to review your code by 0.5 too.

I think that's selling the theorems a little short. A math system with arithmetic is equal to, or more powerful than, a computer. For an example, even classical logic comes with the law of excluded middle that can say (internally) if a program halts or not. Incompleteness applies to all the stronger systems as well.

Null doesn't. `union(Int?, String?)` will only have 1 type of null, unlike a proper discriminated union.

Take your pick :) https://www.templatemaker.nl/en/

Can you set your clock forward or does this also require phoning home to a central server to install an app on your computer?

Here's a version from 2014 in the same style if you're curious: https://web.archive.org/web/20140702092610/https://news.ycom...

They're not doing so here, but shipping a wasm-compiled binary with npm that uses node's WASI API is a really easy way to ship a cross-platform CLI utility. Just needs ~20 lines of JS wrapping it to set up the args and file system.

We guarantee 5 nines of uptime, and 1 nine of not killing people

It's just a regional thing. Neither is correct or wrong. You may as well yell at a french person that the word is "cheese", not "formage".

From the very article you linked:

> In English, the noun mathematics takes a singular verb. It is often shortened to maths or, in North America, math.