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.
I'm fairly skeptical of tests that are closed-book. IMO the only reasons to do so are if 1) the goal is to test rote memorization (which is admittedly sometimes valuable, especially depending on the field) or, perhaps more commonly, 2) the test isn't actually hard enough, and the questions don't require as much "synthesis" as they should to test real understanding.
Admittedly I only know (a little) Japanese and no Korean, but I get the superficial impression that kana are generally much more phonetically faithful than Hangul (namely, because of the post-WWII spelling reform that updated all the kana spellings). Like, the fact that Wiktionary gives "phonetic Hangul" for each Korean entry, to more accurately represent the actual pronunciation, makes me really suspicious of the common internet claim that Hangul is the easiest script to learn.
However, Japanese also has allophony (the moraic nasal and devoicing both come to mind) and kana aren't entirely phonetic (e.g. ha/wa, he/e, ou/ō, ei/ē). I don't know enough about Korean to know if the "irregularities" are also this minor or not—can any Korean speakers/readers enlighten me?
There's an ethos among certain circles (especially on HN, I feel) that basically boils down to "tools don't matter" (perhaps manifesting as "a tool isn't bad if it's ubiquitous" (e.g. Bash or CSS), or "learning curve and footguns don't matter" (e.g. C++)). Of course, it's true that there's a lot of essential complexity to many problems, and hey, maybe CSS really is a local maximum to layout design. And sometimes, a steep learning curve really is inherently necessary, like in functional programming or Rust or what have you. But if a tool is difficult to use due to historical accident, simply accepting that everyone should get good—when more ergonomic alternatives really do exist and are widely used—is simply defeatist. The mere fact that some mental model exists for a tool (in this case, maybe it's "HTML should be semantic") does not necessarily mean it's a good or useful one.
(I say all this as one who's been thoroughly Stockholm syndrome'd by Git, knowing full well that my own argument applies just as much to me in that regard....)
> when more ergonomic alternatives really do exist and are widely used
As someone who got good at Bootstrap, I have to say that Tailwind sucks: it feels like you’re just doing CSS with low-granularity classes. Sure, flexibility, but to the same extent that makes CSS terrible, only now your HTML is littered with inconsistencies.
CSS being nice: one sheet that renders your pages consistent and nice with minimal littering is the markup code.
CSS being sucky: Disconnect between what the CSS codes do, and where they’re used, nearly impossible to clean up, and easy to end up with duplicate efforts.
Bootstrap, for me, strikes the balance better: you do add some classes to the markup, and you get some smart stuff for free, like responsiveness via media queries, but if you want highly configured elements, you extend the CSS; you make a design system and stick to a few custom, high-level classes, and you don’t tack a million classes together at the markup level.
Could you elaborate on the last sentence? Wiktionary claims they're pronounced the same modulo pitch accent, but Wiktionary's phonetic transcriptions are (mostly?) auto-generated AFAIK.
塔 can be pronounced as tou, too, or somewhere between the two. It depends on the speaker, speaking style, and possibly dialect. Either way, Japanese speakers rely more on context and pitch accent than actual pronunciation, so it communicates fine.
No it can't, unless someone is spelling it out, or singing it in a song where it is given two notes, or just hyper-correcting their speech based on their knowledge of writing.
Annoyed speech and such can break words into their morae for empahsis, which breaks up dipthongs.
E.g. angry Japanese five-year-old:
ga kkō ni i ki ta ku nā i!!! (I don't wanna go to school!!!)
"nā i" is not the regular way of saying "nai". The idea that "nai" has that as an alternative pronunciation is a strawman.
You're right. I looked up 現代仮名遣いの告示 [0] for the first time, and it says 塔（とう） is officially pronounced as "too". I had it backwards - I thought that 塔 is "tou", but due to the varying sounds of う, people could (and often preferred to) pronounce it as "too" in everyday speech.
This kind of misconception seems not uncommon. There's an FAQ on NHK's website [1] that addresses the question of whether 言う（いう） is pronounced "iu" or "yuu". The answer is "yuu", and the article make it clear that: "It's not that [iu] is used for polite/careful speech and [yuu] for casual speech - there is no such distinction."
I think native speakers learn words by hearing them and seeing them written in hiragana, before learning the underlying rules, so they know "too" is written as とう, but might not realize that とう shouldn't be pronounced as "tou" or いう as "iu". These are at least less obvious than cases like は in こんにちは never being "ha".
Personally, if I heard someone say 塔 as "tou" or 言う as "iu", I probably wouldn't count it as incorrect, nor would I even notice the phonetic difference.
FWIW I think 言う is a different phenomenon entirely, because おう is pronounced as two vowels when it has grammatical meaning (in this case, as the verb ending), or between different words/morphemes. But my (non-native) understanding was that for nouns and such, or within the main morpheme of a verb (e.g. 葬る), “ou” is (usually) indistinguishable from “oo”.
Another argument I've often heard is that laziness largely obviates macros. Personally, I agree that this is often true—but not always, and that last bit is where Lisp-style macros would be really nice.
do you know of a post or something you could point to that elaborates that argument? interested because I'm having trouble coming up with the line of reasoning on my own
I'm having trouble finding anything concrete online (other than people simply repeating the folk wisdom) other than control flow operators, which are implemented as normal functions in Haskell (i.e. including custom control flow operators).[0] Although, one Reddit comment[1] did also mention typeclasses as obviating other types of macros, so I've edited my earlier comment accordingly.
The venerable master Qc Na was walking with his student, Anton. Hoping to prompt the master into a discussion, Anton said "Master, I have heard that objects are a very good thing - is this true?" Qc Na looked pityingly at his student and replied, "Foolish pupil - objects are merely a poor man's closures."
Chastised, Anton took his leave from his master and returned to his cell, intent on studying closures. He carefully read the entire "Lambda: The Ultimate..." series of papers and its cousins, and implemented a small Scheme interpreter with a closure-based object system. He learned much, and looked forward to informing his master of his progress.
On his next walk with Qc Na, Anton attempted to impress his master by saying Master, I have diligently studied the matter, and now understand that objects are truly a poor man's closures." Qc Na responded by hitting Anton with his stick, saying "When will you learn? Closures are a poor man's object."
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.
reply