lakecresva

12 ms·

91.
by lakecresva 6y ago
The Lean developers put out a paper about v4's reference counting last year which shows that in basic benchmarks, Lean 4 is in the same ballpark as Haskell, Swift, and ML. https://arxiv.org/abs/1908.05647
92.
by lakecresva 6y ago
I like how thinly veiled the doublespeak is these days: “Let me be clear: Productivity Score is not a work monitoring tool,” he added. “Productivity Score ... focuses on actionable insights about the ways in which people and teams are usin
93.
by lakecresva 6y ago
I filed a PR in the nix pills repo like eight months ago that never got touched; they're effectively abandoned and contain hard errors. One more snare trap in the mine field that is nix documentation. To anyone that wanders by this, if
94.
by lakecresva 6y ago
I wrote two reference type checkers for Lean and learned a lot about both the Lean kernel and the implementation of DTT; it's not an easy exercise, but I would recommend it. The ones I wrote are in a language that's not the easies
95.
by lakecresva 6y ago
It's because the mathlib authors don't really care about being constructive and frequently use things like choice/LEM, in contrast to Coq/math-comp. If there's a constructive and non-constructive version of somethin
96.
by lakecresva 6y ago
Can you give a practical example of how denying UIP helps with tasks like writing a proof or a definition rather than defining a really exotic inductive type?
97.
by lakecresva 6y ago
They probably kept most of the $3.2 billion. The burden of proof in civil asset forfeiture cases is on the property owner; in order to get their stuff back they have to prove that they qualify as an "innocent owner". Unless you ha
98.
by lakecresva 6y ago
As bad as all of the proctoring software seems to be, I wish we had it. I'm a 1L at an American law school that's doing entirely unproctored exams. I didn't come to the state with any connections, nor am I friends with any up
99.
by lakecresva 6y ago
This was exactly my experience. They have manuals that are very comprehensive reference texts, but complete lack of structure (no types, no docstrings, no enforced conventions/standards, extremely poor discoverability) makes it a night
100.
by lakecresva 6y ago
I think TLA+ is great, but the way in which you try (here and elsewhere) to downplay its inability to verify implementations/executable code by dismissing an OS kernel and an optimizing C compiler as "tiny programs" make you
101.
by lakecresva 6y ago
He's a person with influence who is endorsing a labor practice. I'm pretty sure no one was ever forced to work for Karl Marx or Adam Smith, yet somehow their opinions on labor managed to affect peoples' working conditions.
102.
by lakecresva 6y ago
Out of curiosity, are you using the vim plugin for VSC? There's only one, but it has a huge install base and causes really insane performance issues in a wide variety of situations. It really should have a disclaimer in its description