To be fair, Japanese headlines use a specific writing style that is much more compressed than normal text, like how English newspaper headlines drop words like “a” or “is” to save space.
The apples one is LLM nonsense: the left example doesn’t include any code for the loop, whereas the streams version actually is iterating over a collection.
Regardless, FP-style code isn’t “shiny new stuff”—it’s been around for decades in languages like Lisp or Haskell. Functional programming is just as theoretically “fundamental” as imperative programming. (Not to mention that, these days, not even C corresponds that closely to what’s actually going on in hardware.)
> Walk! It would be a bit counterproductive to drive a dirty car 50 meters just to get it washed — and at that distance, walking takes maybe 30–45 seconds. You can simply pull the car out, walk it over (or push it if it's that close), or drive it the short distance once you're ready to wash it. Either way, no need to "drive to the car wash" in the traditional sense.
I struggle to imagine how one "walks" a car as distinct from pushing it....
EDIT: I tried it a second time, still a nonsense response. I then asked it to double-check its response, and it realized the mistake.
I got almost the same reply, including the "push it" nonsense:
> Walk! It would be a bit counterproductive to drive a dirty car 50 meters just to get it washed — and the walk will take you less than a minute. You can simply pull the car out and push or walk it over, or drive it the short distance once you're ready to wash it. Either way, no need to "drive" in any meaningful sense for just 50 meters.
When it doesn't, we yearn for something that will fill the void so that it does. It's like that note you yearn for in a musical piece that the composer seems to avoid. One yearns for a resolution of the tension.
Why would N be entitled to it? We made up negative numbers and more just to have a closure. You just learn about them at an age when you don't question it yet.
There are various theories about what's actually happening in quantum mechanics. Some theories have hidden variables, in which case the issue is simply one of measurement (i.e. there really is an "objectively correct" value, but it only looks to us like there isn't).[0] However, this is not known to be the case, and many theories really do claim that position and momentum fundamentally cannot both be well-defined at once. (The "default" Copenhagen interpretation is in the latter camp; AFAIK it's convenient in practice, and as a result it's implicitly assumed in introductory QM classes.)
[0] Well, and the hidden variables are non-local, which is a whole 'nother can of highly non-intuitive worms.
I'm not qualified to say. But, because of inductive reasoning, I have some concern that underneath the next level of "oooh we found the hidden variable" will be a Feynman moment of saying "yea, thats defined by the as-yet unproven hidden-hidden variables, about which much conjecture is being made but no objective evidence exists, but if you fund this very large machine...."
My 2¢ from an interactive theorem proving perspective: In so-called computational type theory, typechecking is indeed allowed to be undecidable, and you get a lot of cool expressive power (e.g. well-behaved quotients and subtypes) as a result. This was one of the big ideas behind NuPRL back in the day, and Istari[0] more recently.
From what I've read, the German phenomenon isn't actually German-specific after all, and English does it too; the difference is just that English keeps the spaces when written. Like, linguists apparently consider "vending machine" to be a perfectly cromulent compound word (among other things, consider that the stress falls on "vending" instead of "machine," which wouldn't(?) happen if "vending" was being used as a bona fide standalone word). Turns out, there's not even an accepted general definition of what a "word" even is in the first place, because different languages vary so much.
The file SSOT.lean is completely trivial, I think: Unfolding the definitions in the theorems, they say nothing but "x=1 => x=1", "x=1 => x≤1", and "x≠1 => x=0 ∨ x>1" (where x is a natural number). Basically, there's no actual proof here, at least not in that file....
This is indeed the danger of letting LLMs manage a "proof" end-to-end—they can just pick the wrong definitions and theorems to prove, and even though the proofs they then give will be formally sound, they won't prove anything useful.
You only read the 37 lines in SSOT.lean and stopped. It's the entry point that defines DOF=1 so other files can import it. The actual proofs are in Foundations.lean (364 lines - timing trichotomy, causality), Requirements.lean (derives the two necessary language features), Completeness.lean (mechanism exhaustiveness), Derivation.lean (the uniqueness proof that achieves_ssot m = true iff m = source_hooks), Coherence.lean, CaseStudies.lean, LangPython.lean, LangRust.lean etc.
~2k lines total across the lean files. Zero sorry. Run grep -r "sorry" paper2_ssot/proofs/ if you don't believe me.
"Unfolding the definitions they say x=1 => x=1" applies to three sanity lemmas in the scaffolding file. It's like reading __init__.py and concluding the package is empty.
Fair, the em dash comment was a cheap shot. Withdrawn.
The substantive point stands: you've now "skimmed" multiple files, called them all "boilerplate," and haven't engaged with the actual proof structure. The rebuttals section addresses "The Proofs Are Trivial" directly (Concern 9).
At some point "I skimmed it and it looks trivial" stops being a critique and starts being "I didn't read it."
I also took a look at the `LangRust.lean`, and the majority of the proofs are just `rfl` (after an `intros`)—that's a major red flag, since it means the "theorems", like those in SSOT.lean, are true just by unfolding definitions. In general, that's basically never true of any interesting fact in programming languages (or math in general); on the contrary, it takes a lot of tedious work even to prove simple things in Lean.
Yes, many proofs are rfl. That's because we're doing engineering formalization, not pure math. The work is in getting the definitions right. Once you've correctly modeled Rust's compilation phases, item sources, and erasure semantics, the theorem that "RuntimeItem has no source field, therefore query_source returns none" should be rfl. That's the point.
The hard part isn't the proof tactics. The hard part is:
- Correctly modeling Rust's macro expansion semantics from the language reference
- Defining the compilation phases and when information is erased
- Structuring the types so that the impossibility is structural (RuntimeItem literally doesn't have a source field)
If the theorems required 500 lines of tactic proofs, that would mean our model was wrong or overcomplicated. When you nail the definitions, rfl is the proof.
Compare to software verification: when you prove a sorting algorithm correct, the hard work is the loop invariants and the model, not the final QED. Tedious proof steps usually indicate you're fighting your abstractions.
The real question isn't "are the proofs short?" It's "can you attack the definitions?" The model claims RuntimeItem erases source info at compile-to-runtime. Either produce Rust code where RuntimeItem retains its macro provenance at runtime, or accept the model is correct. The rfl follows from the model being right.
> Compare to software verification: when you prove a sorting algorithm correct, the hard work is the loop invariants and the model, not the final QED. Tedious proof steps usually indicate you're fighting your abstractions.
This is a false statement when working with an interactive theorem prover like Lean. Even trivial things require mountains of effort, and even blatantly obvious facts will at least require a case analysis or something. It's a massive usability barrier (and one that AI can hopefully help with).
This is addressed in the paper's Preemptive Rebuttals section (Concern 9: "The Proofs Are Trivial").
At 2k lines of lean, the criticism was "these proofs are trivial." At 9k lines of lean with 541 theorems, the criticism is... still "trivial"? At what point does the objection become "I didn't read it"?
The rfl proofs are scaffolding. The substantive proofs (rust_lacks_introspection, Inconsistency.lean, Coherence.lean) are hundreds of lines of actual reasoning. This is in the paper.
Keyboards are highly deterministic. And when they're not, e.g. due to physical wear or software glitches, this makes them basically unusable for touch typists.
reply