So then if the BB sequence has finitely many entries. What does it mean that it grows faster than any computable sequence? A finite sequence can't have any asymptotic behavior right?
The BB sequence still has infinitely many entries. Any turing machine will either halt or not halt. For any N, there is a finite set of N-state turing machines which halt, and there is therefore a finite number of steps after which all halting N-state turing machines would halt.
There is a point where these values become uncomputable, but they still exist (for some definition of exist).
I am not sure I follow? But maybe I misunderstood your quote. It seems any given TM (And for a fixed N, there are only finite many), there are only the two option: it halts, or it doesn't halt. There is no third option?
Of course, the question whether you can proof that it doesn't halt, in ZF or ZFC, is a different question. (You can always proof that it halts if you know that it halts. You run it until it halts)
I'm not entirely sure about what I'm unsure about, but I think I struggle to accept that there is truth beyond the axioms. Like in my mind if the axioms can't prove whether it halts or not then that's that. There is no "but actually it doesn't halt". Or at least that's where my current thinking is, I think?
I do lack a lot of knowledge about the concept of interpretation, so maybe that's where my issue is?
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)
You should be able to prove it by showing that the existence of a faster-growing computable function lets you solve the halting problem.
Assume f(x) is computable and grows faster than BB(x). We can create a computable g(x) where g(x) > BB(x) for all x, by setting g(x) = f(x) + C for some suitable constant.
Now we create a computer program that does the following. 1. Get the size of the input program and compute g(n). 2. Run the input program for g(n) steps. 3. If it stopped, return true. If it's still running, return false.
This solves the halting problem. Since a computer program can't solve the halting problem, this program can't exist. Everything except "compute g(n)" is straightforward, so there must be no such function g, and no such function f.
Where did you get that the BB sequence would have finitely many entries? You can choose any integer n for BB(n), and there are infinitely many integers.
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.
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.
And a patch panel and a bunch of patch cables that you plug in and out to construct your pipelines.
And eventually hire people whose job it is to patch pipelines on demand for everyone in the office.
“Hey Jim, I’m gonna output the systemd logs of nginx on line five, can you assemble a grep pipeline for me to match all HTTP 500 status codes from /api/cart POST request log lines? Connect the filtered output to Tim’s desk, line 7. He’s there now, we are trying to figure something out.”
I wonder how close you can get with Nvidia's GPUDirect. Hook the fast NVME directly up to the GPU (well, it gets direct DMA to GPU at any rate), then implement parallel grep in CUDA... profit?
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.
This whole week I've been dealing with incidental complexity created by shortcuts taken and edge cases not handled in code written in the before times, both in mine and in others'. I realized at some point yesterday that these kinds of shortcuts would no longer be accepted with competent LLM use.
Right, when used incompetently. When used competently they can carefully reason through every edge case and flag things no human would have picked up on.
One example: in some old code I wrote I had assumed that the Rust Hash impl for a type is stable over time. This is not the case in general, but writing a custom hasher for a complex type is incredibly annoying, so I took that shortcut. That was fine for years, but came back to bite me this week as I was trying to update a dependency.
How much incidental complexity is due to that kind of thing? An LLM code review would flag this instantly, and one would also write a stable hash function for you.
The mental model was required when your brain was the only chance to reason about changes, answer cross-cutting questions (architecture), and develop a visceral feel for the project, because that's what you needed to write high quality software
It's hard to let that go, but you already had to in larger human organizations/collaborations where you might be assigned work on systems you never/seldom touch, or coming back to a project you haven't touched in a long time.
You don't need a mental model when you can automate the reasoning and the benchmarks that vet the reasoning. Your mental model is better spent pondering->reconsidering high level things like invariants, and then automating the the proof and implementation of those decisions.
Consider how you can just get Claude to start a workflow of 15 Fable agents to fan out over your system looking for correction/simplification/perf opportunities before spawn another wave of agents to vet the list of findings. How much time and energy and studying of the code would it have taken you to build and vet the same list?
Have you looked at the machine instructions your compiler produces?
No? Why?
Because software languages are a pretty good abstraction.
To the extent that good abstractions are in place, you can avoid looking at code specifically.
Those don't perfectly well exist, so it takes a lot of self discipline and the right tools/methods, but invariably, AI will produce better systems.
That said, its very easy to produce slop, so well see much more of it.
But mostly, it will be AI from here on in, as a matter of productivity. There are some arguments on the margins but those will fade over the next few years.
'At minimum' - the 'power tools' are here to stay.
LLMs are pretty much the exact opposite of a reliable compiler-like abstraction.
This is true to such an extent that I have to question the overall competence of anybody who makes the comparison. It's an enormous red flag.
I'd recommend reading Joel spolsky's leaky abstractions essay coz while it applies less and less 20 years later to things like kernel abstractions it explains very well why treating the LLM as a compiler sets you up for abject failures.
A compiler translating high-level code to machine code is a predictable and repeatable process.
An LLM translating a prompt to to high-level code has a much lower degree of predictability. To say an LLM prompt is a comparable abstraction is unfair, though I admit it's getting very close.
I don't get the use of "abstraction" in this context, I must admit.
Programming abstractions offer interfaces to functionality that are both simplified in use and restricted in capability. (e.g. any API or compiler.) I don't see how LLMs meet that definition.
It seems more like we're talking about offloading or delegation, here. And that's a valid business tactic, certainly, but it's not a software abstraction any more than a CTO is an abstraction of a tech lead, no?
> But yes, it has to fulfill some kind of contract defined by the absraction.
I don't follow. Is the contact here the design specification for the system? If so, again, I'd argue that's not an abstraction.
An abstraction could be a design requirement, expressed in some way.
That's definitely an abstraction.
IDLs are a form of abstraction, they're a requirement somewhat more formally described.
Remember UML? That was an attempt to go 1/2 layer above the code, that was an abstraction.
There were tons of tools like that.
APIs are an abstraction - maybe the best example. We write code to match exactly the behaviour defined by an APU - as long as it meets the requirement of that contract, then 'it's good'. And there could be many ways of doing that.
Higher level languages are still formal languages. I think there's a conceptual difference between moving from one formal language to another (machine instructions to asm or asm to C) and moving from a formal language to natural language. So yes, developing, looking at and understanding a formal description of your system has benefits for an engineer compared to handing off this step completely.
Sure but you only look at it when optimizing some performance critical code, usually the hot path. That is usually a tiny fraction of the codebase. I also use AI to generate large amounts of code but I only inspect the actual code when critical, delicate or architecturally important stuff is involved.
If you're doing high performance Java you're definitely looking at the compiler output. At least you should be.
It's arguably more important with Java than with the compiler output for something like C++, as C2 is much more unpredictable and dependent on runtime circumstances. You also want to be real certain that bounds and null checks are omitted as those come at a pretty big performance premium.
> Have you looked at the machine instructions your compiler produces?
> No? Why?
> Because software languages are a pretty good abstraction.
No, it’s because compilers produce deterministic output. I am so tired of this argument.
If I’m not concerned with the performance of my code, I can be 100% confident that that exact code will produce the correct assembly every time. That’s why I don’t read it. Not because I don’t care.
No, determinism is actually required. If compilers changed between producing decent assembly and crap assembly from run to run, we would be reading the generated assembly every single time.
Yall modern compilers do not produce the same thing every time. Compilers have had decades to get really good at what they do. LLMs have been functional for maybe 3 years?
https://scottaaronson.blog/?p=2725