This isn't really a metric. It's a description to help the reader understand the magnitude of effort that went into this project. SLoC is a bad metric for plenty of things, but I think it's fine for quickly conveying the scope of a project to a blog reader.
Do you remember writing the proof for quicksort, which is say 0.1k lines? 15k lines of verified code is a pretty good indication of effort.
But the problem may come from the headline, which is somewhat clickbaity. HN forbids changing it, and then part of the discussion focuses on the literal content of the headline, which is, as you rightly hint, not the best summary of what's interesting here.
> A 15,000-line proof is going to have a mistake somewhere.
If this proof is formal, than it is not going to. That is why writing formal proofs is such a PITA, you actually have to specify every little detail, or it doesn't work at all.
> Verifying that those 15,000 lines do what they do doesn't give me much more confidence than thorough unit testing would.
It actually does. Programs written in statically typed languages (with reasonably strong type systems) empirically have less errors than the ones written in dynamically typed languages. Formal verification as done by F* is like static typing on (a lot of) steroids. And HACL has unit tests among other things.
You're presuming that every phrase was worded _just so_. This could very well have been from the author refactoring their sentence and not simplifying everything. They probably were thinking in these terms (the author is a PL guy from MSR who's pretty heavy into a lot of the formalism) and this sounds like a not-perfectly-polished formal thought.
It's technical, and sometimes technical writing isn't written perfectly. That doesn't mean it's due to willful obtusity, or trying to sound smart.
Meh, it's usable w/out github but you'll be reading raw markdown files (unless you get your own markdown renderer which isn't that big of a deal). But yeah, it's either an incomplete git-based wiki or a complete github based wiki.
I found In My Room to be an incredibly moving album. Djesse left me feeling far less after a first listen, but when I returned a few days later I started to notice things I had missed and now I really enjoy that album as well.
I am very moved by his music, in large part because of its cleverness. At the same time, I completely understand why many people are left unmoved. Different strokes, I guess.
There should also be a Latex library (?) that makes your documents look like they were photocopied, so you can use the coffee stains and the photocopy to make it look like you spent long nights working on your assignments.
Haha that first one's great, addresses (what is sadly) a real need.
I've seen that cthulhu-worshipping madman one before, but the results are disappointing. I'm sure much better can be done in that direction. e.g. (is this the most famous SE answer of all-time?) https://stackoverflow.com/questions/1732348/regex-match-open...
Pizza gate is an extreme. But also, yes, news has changed dramatucally over the last couple of decades and older generations maybe don't consume as defensively as younger generations. Over time this can make ridiculous things sound plausible.
I remember there was a trump meme going around where he supposedly said "if I ever ran for president it would be as a republican, they are all a bunch of morons". The first time I saw that it looked sketchy as hell, but both of my folks (intelligent people, mind you) bought it hook, line, and sinker. In general, it's younger people that I saw citing it as a fake while older people shared it. Totally anecdotal, I'll grant you, but I hardly think my experience is unique
I don't think it's that ridiculous things can sound plausible. No, they sound ridiculous. I think it's when the fake news looks like something someone is inclined to believe anyway. In my little bubble, I'm always chiding young, progressive friends for uncritically sharing memes with fake quotes etc that happen to reinforce their political biases.
I don't know, I might push back here. While fake news can certainly be interpreted as news that is false, that is not how it is usually used. There is definitely an insinuation, and while the vanilla reading of the definitions of "fake" and "news" don't contain this insinuation, it exists none the less.
That being said, as a writer I might not be able to resist pointing out the irony that the paper on fake news was fake news :). I really can't fault the author.
