https://github.com/jgrosso
- BalinKing parentYeah, I'm on macOS (although even back on Windows, I used to use the Character Map all the time).
- > 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).
- 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.
- 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.
- 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....)
- 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”.
- 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.
[0] https://www.reddit.com/r/haskell/comments/5xge0v/comment/deh...
[1] https://www.reddit.com/r/haskell/comments/1929xn/comment/c8k...
- Honestly, the SCP wiki might scratch this itch for you—it's sci-fi but with a lot of fantasy elements, and I'd put it on the "hard" side of the spectrum. Also, I think Greg Egan's books are pretty out there (the two I've read are Diaspora and Permutation City, whose settings aren't particularly "plausible" IMHO), and they really make you think.
- To echo the sibling comment, that answer is specifically referring to the type theory behind Lean (which I’ve heard is pretty weird in a lot of ways, albeit usually in service of usability). Many type theories are weaker than ZFC, or even ZF, at least if I correctly skimmed https://proofassistants.stackexchange.com/a/1210/7.
- https://news.ysimulator.run/item/1292
> Give it a few more hours and this will devolve into a pedantic grammar autopsy, three parallel threads arguing about whether the title is “technically correct,” and someone linking a 30-year-old Usenet post. Then a latecomer will ask why this is on HN at all, as if that ever helped.
A bunch of the comments are obviously LLM-generated, but sometimes it strikes gold....
- Thanks for the thoughtful response!
Not necessarily trying to debate or anything—clearly you've put a lot of intellectual effort into this over the years already—but I find one point you made particularly interesting. (Disclaimer: I am a Christian.) Namely, that "religious people will freely admit their beliefs have no evidence." There are some (many?) religions where this is the case, but I honestly don't think Christianity is one of them—the Bible puts a strong emphasis on evidence. For example:
- The gospels themselves are composed of three primary sources as well as a secondary source.
- Jesus made specific prophetic claims (famously, the destruction of the Second Temple in Mark 13:2, or that he would be crucified in Matthew 20:18-19).
- 1 Corinthians 15:6 references more than five hundred eyewitnesses, most of whom were claimed to be still living.
- Acts 17:17 describes Paul as "reasoning" with secular Greek philosophers (instead of merely, say, "moralizing" or "persuading"), although I suppose these discussions may have been more philosophical than empirical given the Greeks' philosophical bent.
- The gospels claim that even the Pharisees did not deny Jesus' miracles, but merely attributed them to malign influence (Mark 3:22) or just decided to kill him (Matthew 12:14).
- Jesus' parable in Luke 16:19–31 implies that for some people, getting more evidence will not actually change their minds, regardless of how persuasive it would be.
Of course one could (and should) argue that an emphasis on historicity is not itself evidence; but I just wanted to point out that Christianity is not one of the religions where you just have to believe blindly. On the contrary, the Bible presents unbelief in the face of evidence as a main obstacle between us and God (cf. Romans 1:18–20).
- I disagree, because with an instrument you actually get music out at the end, which is enjoyable in its own right on top of the satisfaction of executing the technical challenge of playing it. A more akin analogy, in my opinion, would be “any musical instrument which has been artificially muted”—this could definitely still be fun, and indeed I’ve played my keyboard without sound before, but it really doesn’t compare.
- I want to push back on this, because the Christian conception of God definitely includes the idea that God created all good and comforting things, and is indeed their ultimate source. Like, just because God is transcendent[0] does not mean He cannot create things that are perfectly approachable, understandable, and enjoyable.
[0] Jesus being human changes the calculus quite a lot, of course, as elaborated in e.g. Hebrews 4:14–16. God, who was fully transcendent, became human, hence why Jesus is also called Immanuel/Emmanuel (lit. “God with us”) in the Bible.