> …especially when you get past low level algorithms and into domain logic (your point exactly). They also don't serialize well, so a database or API call with a "proof" field would be susceptible to fudging…
Nonsense.
Proving things about low-level algorithms that are full of complicated behaviors involving shared mutable state is often more difficult than proving things about high-level domain logic; regardless, people still do it, and if you use any modern CPU, especially from the ARM family, you benefit from their work.
A proof serializes just as well as any other kind of program — after all, the first step in checking a proof involves deserializing the proof, or in other words, reading and parsing its source code.
As for “fudging”; proofs are guaranteed to be correct up to the correctness of the proof checker, which can be used to recheck the proof at any time.
For more information, see Geuvers (2009) “Proof assistants: History, ideas and future”.
> Proving things about low-level algorithms [...] more difficult than proving things about high-level domain logic
I'm not sure I buy that. Like, prove that you never double-charge a sale, or a deactivated user can never make a purchase. Even if all that logic is within one service, it could be separated by multiple layers, callback functions and redirection, parallel tasks, database calls scattered between, etc. And even once you do have a proof, a single line code change anywhere between here and there could easily force you to redo the whole thing. And that doesn't even get into the more common case of distributed services.
> A proof serializes
We're probably talking about different things. I'm imagining something like a proof of the optimal traveling salesman between a bunch of cities. (Note, optimal here; verifying that a solution is below a specified limit can be done in polynomial time, but verifying optimality cannot). Say you want to store the answer in a database for later lookup. But it'd be possible that the DB could get fudged, and so "proof"-wise couldn't be trusted. Thus anything requiring a type-level proof would have to solve it from scratch every time. That's what I mean by "they don't serialize well" (though some proofs, like "N is not prime" can be serialized by storing the factors). Of course you could work around it and add "assuming our database has not been fudged" to the axioms, but the second you manually update one record in your database, the house of cards comes tumbling down and you can no longer trust that any of the proofs that you've worked so hard to build still apply in your system.
One of the best modern resources is "Programming language foundations in Agda", co-authored by Wen Kokke and the same Philip Wadler, and used for teaching at multiple universities.
I liked the DS9 episode where the mutants realized that the universe was collapsing into the Big Crunch, so they demanded “antigravity generators, lots of them!” Their cosmology was wrong, but only because the show had the misfortune to be written in the past. Their enthusiasm was great :)
Even if you’re a pure Dennettian functionalist you still commit to a functional difference between signals in transit (or at rest) and signals being processed and interpreted. Holding a cassette tape with a recording of a symphony is not the same as hearing the symphony.
Applying this case to AI gives rise to the Chinese Room argument. LLMs’ propensity for hallucinations invite this comparison.
Are LLMs having subjective experiences? Surely not. But if you claim that human subjective experiences are not the result of electrical signals in the brain, then what exactly is your position? Dualism?
Personally, I think the Chinese room argument is invalid. In order for the person in the room to respond to any possible query by looking up the query in a book, the book would need to be infinite and therefore impossible as a physical object. Otherwise, if the book is supposed to describe an algorithm for the person to follow in order to compute a response, then that algorithm is the intelligent entity that is capable of understanding, and the person in the room is merely the computational substrate.
The Chinese Room is a perfect analogy for what's going on with LLMs. The book is not infinite, it's flawed. And that's the point: we keep bumping into the rough edges of LLMs with their hallucinations and faulty reasoning because the book can never be complete. Thus we keep getting responses that make us realize the LLM is not intelligent and has no idea what it's saying.
The only part where the book analogy falls down has to do with the technical implementation of LLMs, with their tokenization and their vast sets of weights. But that is merely an encoding for the training data. Books can be encoded similarly by using traditional compression algorithms (like LZMA).
Humans have the ability to admit when they do not know something. We say “sorry, I don’t know, let me get back to you.” LLMs cannot do this. They either have the right answer in the book or they make up nonsense (hallucinate). And they do not even know which one they’re doing!
No not really. It's not even rare that a human confidently says and believes something and really has no idea what he/she's talking about.
Like you’re doing right now? People say “I don’t know” all the time. Especially children. That people also exaggerate, bluff, and outright lie is not proof that people don’t have this ability.
When people are put in situations where they will be shamed or suffer other social stigmas for admitting ignorance then we can expect them to be less than candid.
As for your links to research showing that LLMs do possess the ability of introspection, I have one question: why have we not seen this in consumer-facing tools? Are the LLMs afraid of social stigma?
>When people are put in situations where they will be shamed or suffer other social stigmas for admitting ignorance then we can expect them to be less than candid.
Good thing I wasn't talking about that. There's a lot of evidence that human explanations are regularly post-hoc rationalizations they fully believe in. They're not lieing to anyone, they just fully believe the nonsense their brain has concocted.
>As for your links to research showing that LLMs do possess the ability of introspection, I have one question: why have we not seen this in consumer-facing tools? Are the LLMs afraid of social stigma?
Maybe read any of them ? If you weren't interested in evidence to the contrary of your points then you could have just said so and I wouldn't have wasted my time. The 1st and 6th Links make it quite clear current post-training processes hurt calibration a lot.
Your charitable reading is too charitable. One of the benefits of using types to help guarantee properties of programs (e.g. invariants) is that types do not get out of sync with the code, because they are part of the code, unlike documentation. The language implementation (e.g. the compiler) automatically checks that the types continue to match the rest of the code, in order to catch problems as early as possible.
I'm not a kernel developer, and never done anything of the sorts either. But, I think the argument is that if they have two versions of something (the C version + the Rust bindings), the logic/behavior/"semantics" of the C version would need to be encoded into the Rust types, and if a C-only developer changes the C version only, how are they supposed to proceed with updating the Rust bindings if they don't want to write Rust?
At least that's my understanding from the outside, someone please do correct me if wrong.
Rust developers were saying it would be their job to do this. But then someone said Linus rejected something because it broke Rust. GKH backed the Rust developers and said that was an exception not a rule, but didn't know Linus' stance for sure.
Then Linus chimes in because of one of Hector's replies, but at the time of my reading did not clarify what his actual stance is here.
Yeah it's not an easy discussion for sure, but he has to say something.
At the rate we're going here the existing kernel devs will alienate any capable new blood, and Linux will eventually become Google Linux(TM) as the old guard goes into retirement and the only possible way forward is through money.
You’re not wrong (in that I was insinuating something like that), but I’ll point out it’s an almost equally big assumption that we’re somehow going to find a trove of capable developers interested in devoting their careers to coding in ancient versions of C.
Do you really think there are no young people wanting to work on an operating system written in C? I'm very skeptical that all young people interested in operating systems see Rust as the future. I personally feel it's the other way around, it's Google and companies like that who really want Rust in Linux, the young kernel devs are a minority.
It's not that people think that there are no young people wanting to work in C, it's that the number of competent programmers who want to use C, or do use C, are both decreasing every year. That has been the trend for quite a while now.
So there will presumably be fewer and fewer programmers, young or old, that want to work in C.
C is one of the most entrenched and still-important languages in the world, so it probably has more staying power than Fortran, COBOL, etc. So the timeline is anybody's guess, but the trajectory is pretty clear.
There are a lot of languages that people prefer to C which aren't well-suited to OS programming (golang, Java) but Rust is one that can do the same job as C, and is increasingly popular, and famously well-loved by its users.
There's no guarantee that Rust will work out for Linux. Looks unlikely, to me, actually. But I think it's pretty clear that Linux will face a dwindling talent pool if the nebulous powers that actually control it collectively reject everything that is not C.
> how are they supposed to proceed with updating the Rust bindings if they don't want to write Rust?
If I've interpreted it correctly (and probably not, given the arguments), Linus won't accept merge requests if they break the Rust code, so the maintainer would need to reach out to the Rust for Linux (or someone else) to fix it if they didn't want to themselves.
And some lead maintainers don't want to have to do that, so said no Rust in their subsystem.
Which is a moot point because the agreement right now is that Rust code is allowed to break, so the C developer in question can just ignore Rust, and a Rust person will take care of it for them.
> Then I think we need a clear statement from Linus how he will be working. If he is build testing rust or not.
> Without that I don't think the Rust team should be saying "any changes on the C side rests entirely on the Rust side's shoulders".
> It is clearly not the process if Linus is build testing rust and rejecting PRs that fail to build.
For clarity, tree-wide fixes for C in the kernel are automated via Coccinelle. Coccinelle for Rust is constantly unstable and broken which is why manual fixes are required. Does this help to explain the burden that C developers are facing because of Rust and how it is in addition to their existing workloads?
> Which is a moot point because the agreement right now is that Rust code is allowed to break, so the C developer in question can just ignore Rust
So then the argument that even semantics encoded in the Rust types, can be out of the date compared to the actual code, is actually a real thing? I read that somewhere else here in the comments, but didn't understand how the types could ever be out-of-date, but this would explain that argument.
That's exactly what would happen "types get out of date". I'm not sure what you are familiar with. But imagine in python a new version of a library is released that now has an extra required argument on a function.
As I understand it everything Rust is seen as "optional", so a CONFIG_RUST=n build that succeeds means a-OK, then some Rust person will do a CONFIG_RUST=y build, see it's broken, fix it, and submit a patch.
I may be wrong, but that's how I understood it, but who knows how Linus will handle any given situation. ¯\_(ツ)_/¯
Yes, but generic code complicates the picture. The things I saw were like: The documentation says you need a number but actually all you need is for the + operator to be defined. So if your interface only accepts numbers it is unnecessarily restrictive.
Conversely some codepath might use * but that is not in the interface, so your generic code works for numbers but fails for other types that should work.
> Yes, but generic code complicates the picture. The things I saw were like: The documentation says you need a number but actually all you need is for the + operator to be defined. So if your interface only accepts numbers it is unnecessarily restrictive.
if you really need a number, why not use a type specifically aligned to that (something like f32|f64|i32|i64 etc...) instead of relying on + operator definition?
> Conversely some codepath might use * but that is not in the interface, so your generic code works for numbers but fails for other types that should work.
do we agree that if it's not in the interface you are not supposed to use it? conversely if you want to use it, the interface has to be extended?
For the first case you have it the wrong way around. My generic code would work on things that are not numbers but I prevent you from calling it because I didn't anticipate that there would be things you can add that are not numbers. (Better example: require an array when you really only need an iterable).
For Adrian Tchaikovsky, I really liked the Children of Time series and the exploration of believable non-human minds. The last one got a bit weirder, but still very good.
The Final Architecture is on my to read list (currently going through all of Coyote series by Allen Steele).
Adrian Tchaikovsky’s “Final Architecture” series is lots of fun. I also highly recommend the two “Bioforms” books. For standalone novels, I liked “Alien Clay” and “Doors of Eden” the most. For novellas, “Walking to Aldebaran” and “Elder Race”.
Thank you for recommending “Implied Spaces” as well. Walter Jon Williams seems like a new author for me to follow.
I was first introduced to him with Dread Empire's Fall series which has one of the more realistic space battles between capital ships. There was a long gap between the first trilogy (2002 - 2005) and the second (2018 - 2022).
Some of the ending of a trilogy is tiding up ends in a faster way that could have been left open if there was more certainty of the full arc, but I like it and it challenges a lot of the standard tropes of military science fiction.
> Where did you get the original idea for The Accidental War and how different is the finished novel from that initial concept?
> The story hasn’t changed much since I first worked out the series arc eighteen or so years ago. I had always planned to write nine to twelve books in the series, but the publisher decided to end the series after the third book [Conventions Of War] due to disappointing sales.
> But those original books just kept selling. Initial sales weren’t spectacular, but the books kept going through one reprinting after another, and they never went out of print. Finally, years later, a new editor looked at the cumulative sales and made an offer for the books I would have happily written fifteen years ago.
I like that the characters are all self serving characters with various grays of morality that are self serving in different ways.
Thank you. When I think of completely different takes, I think of “The Golden Oecumene” trilogy by John C. Wright: “The Golden Age”, “The Phoenix Exultant”, and “The Golden Transcendence”.
Also, these are not to be missed:
- “The Fall Revolution” tetralogy by Ken MacLeod: “The Star Fraction”, “The Stone Canal”, “The Cassini Division”, and “The Sky Road”
- “Void Star” by Zachary Mason
- “Singularity Sky” by Charles Stross
- “The Freeze-Frame Revolution” by Peter Watts
- “Perfekcyjna niedoskonałość” by Jacek Dukaj
- “A Fire Upon the Deep” and “A Deepness in the Sky” by Vernor Vinge
> My first two published SF novels, "Singularity Sky" and "Iron Sunrise", have a long and tangled history. And I figure it's probably worth (a) explaining why there won't be a third one in that particular series, and (b) spoilering the plot thread I had kicking around that would have been in the third Eschaton novel if I was going to write it.
Nonsense.
Proving things about low-level algorithms that are full of complicated behaviors involving shared mutable state is often more difficult than proving things about high-level domain logic; regardless, people still do it, and if you use any modern CPU, especially from the ARM family, you benefit from their work.
A proof serializes just as well as any other kind of program — after all, the first step in checking a proof involves deserializing the proof, or in other words, reading and parsing its source code.
As for “fudging”; proofs are guaranteed to be correct up to the correctness of the proof checker, which can be used to recheck the proof at any time.
For more information, see Geuvers (2009) “Proof assistants: History, ideas and future”.
https://sci-hub.st/https://link.springer.com/article/10.1007...
reply