cwzwarich

7 ms·

31.
by cwzwarich 2y ago
Well, the first thing to realize about scaling codebases with developers is that an N developer team will usually produce a codebase that requires N developers to maintain. So by starting small and staying small until you reach a certain cr
32.
by cwzwarich 2y ago
> May I ask, what is the path that leads you to the Rosetta 2 project? The member of senior management who was best poised to suggest who should work on it already knew me and thought I would be the best choice. Getting opportunities in
33.
by cwzwarich 2y ago
I don't think there was a single tipping point, just a growing accumulation of factors: - the release of Lean 4 slightly over a year ago, which impressed me both as a proof assistant and a programming language - the rapid progress in f
34.
by cwzwarich 2y ago
I was the only person working on it for ~2 years, and I wrote the majority of the code in the first version that shipped. That said, I’m definitely glad that I eventually found someone else (and later a whole team) to work on it with me, an
35.
by cwzwarich 2y ago
If you’re interested in applications of AI to mathematics, you’re faced with the problem of what to do when the ratio of plausible proofs to humans that can check them radically changes. There are definitely some in the AI world who feel th
36.
by cwzwarich 2y ago
https://lean-fro.org/about/
37.
by cwzwarich 2y ago
This is me! Didn’t expect to see this on here, but I’m looking forward to working with everyone else at the Lean FRO and the wider Lean community to help make Lean even better. My background is in mathematics and I’ve had an interest in int
38.
by cwzwarich 2y ago
The example in this blurb is a pretty good one: https://www.hboehm.info/c++mm/why_undef.html
39.
by cwzwarich 2y ago
If your LLM is producing a proof that can be checked by another program, then there’s nothing wrong with their reliability. It’s just like playing a game whose rules are a logical system.
40.
by cwzwarich 2y ago
According to the linked proposal, these implicit capability parameters are lexically bound, not dynamically bound.
41.
by cwzwarich 2y ago
> You can set a global FPU flag at the start of the program to force rounding on every operation This doesn’t do quite the same thing. It still uses the wider exponent range of the 80-bit type.
42.
by cwzwarich 2y ago
The fringe nature of this hypothesis is discussed in the article itself. I was just explaining why one would even think to go down this road to begin with.
43.
by cwzwarich 2y ago
Most people who encounter Yiddish outside of the religious Jewish community encounter Western Yiddish. Most people who learn Yiddish as a first language today would be speaking Eastern Yiddish (think Ukraine, Belarus, Lithuania, Russia), wh
44.
by cwzwarich 2y ago
I’m confused. Wasn’t the error actually in an unverified subsystem and isomorphic to an error caught by the model checker in a verified subsystem? Isn’t this more of a cautionary tale for someone not relying on formal verification?
45.
by cwzwarich 2y ago
> For this particular question we have a great answer in the form of homotopy type theory. It handles all the complications that the author mentions. This is one of the reasons type theorists were excited about HoTT in the first place. A
46.
by cwzwarich 2y ago
I wrote my own build system to use C++20 modules before CMake even had support for them, and while I have probably had net benefit from using them, I can’t recommend them for anyone in their own projects at this point. The feature has so ma
47.
by cwzwarich 2y ago
If I’m not mistaken, this is the first use of a proof assistant to settle the status of a difficult proof that had been sitting in limbo for years. There were some previous projects (e.g. the Four Color Theorem in Coq) that validated existi
48.
by cwzwarich 3y ago
I was specifically referring to the ability to borrow a set of fields/paths. Enabling more useful self-referential structs would be something more novel.
49.
by cwzwarich 3y ago
The Rust borrow checker has had this model for over a decade at this point; it's just not exposed as part of the language. One strong principle in Rust language design is to avoid proliferation of too many distinct reference types. In
50.
by cwzwarich 3y ago
As a counterpoint, Wirth-style languages have basically remained the same for decades whereas work on type theory has repeatedly moved the boundaries of comprehensibility.
51.
by cwzwarich 3y ago
> (see, eg., google's carbon which iirc, seeks to be ast-free single-pass) Carbon’s (mostly hypothetical) frontend is actually 3 passes: lexing, parsing, and a semantic analysis pass, each with separate IRs. One of their arguments i
52.
by cwzwarich 3y ago
> Mathjax, mathml and stuff are less than 10 years old MathML is from the 90s and MathJax is from 2009.
53.
by cwzwarich 3y ago
Here is the original GitHub issue on the question: https://github.com/rust-lang/rust/issues/15699 And an RFC by some people that felt frustrated by this arguably implementation-centric view that kind of lost
54.
by cwzwarich 3y ago
`static is actually the superlifetime of all lifetimes, but & is contravariant in its lifetime parameter (and covariant in its type parameter).
55.
by cwzwarich 3y ago
Godel’s collected works (including much unpublished work and correspondence) have been published by Clarendon Press, with more work (including translations from German) put into them than pretty much any other mathematician’s collected work
56.
by cwzwarich 3y ago
The one way in which they are slower than headers is that they create longer dependency chains of translation units, whereas with headers you unlock more parallelism at the beginning of the build process, but much of it is duplicated work.
57.
by cwzwarich 3y ago
> What would Servo bring to make web a big jump forward for us users The biggest advantage would be having a memory-safe browser engine.
58.
by cwzwarich 3y ago
> Why aren't we collectively putting our time/effort etc.. into making Firefox the singular and best FOSS browser ever? [disclaimer: former Servo team member] Mozilla had a chance to advance browser tech with Servo and fumbled
59.
by cwzwarich 3y ago
One advantage C++ has over Rust is that there are multiple fairly compliant C++ implementations, and the process of making them created some shared understanding of how the language actually works from an implementation perspective. There a
60.
by cwzwarich 3y ago
The beamer class has a [handout] option, which at least attempts to do this (with some corner cases IIRC, but it's been a while).

More ›