cwzwarich

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 critical mass of fundamental decisions, you can avoid some of the problems that you get from having too many developers too early. You can easily also fall into the reverse trap: a historical core with pieces that fit too well together, but most of the developers on the team don’t intuitively understand the reasons behind all of the past decisions (because they weren’t there when they happened). This can lead to poorly affixed additions to a system in response to new features or requirements.

As far as Rosetta in particular was concerned, I think I was just in the right environment to consistently be in a flow state. I have had fleeting moments of depression upon the realization that I will probably never be this productive for an extended period of time ever again.

> 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 large companies is a combination of nurturing relationships and luck.

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 formalization of mathematics from 2017 onward, almost all of which was happening in Lean

- the growing relevance of formal reasoning in the wake of improvements in AI

- seeing Lean's potential (a lot of which is not yet realized) for SW verification (especially of SW itself written in Lean)

- the establishment of the Lean FRO at the right time, intersecting all of the above

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, and it wouldn’t have been as successful without that.

When people think of a binary translator, they usually just think of the ISA aspects, as opposed to the complicated interactions with the OS etc. that can consume just as much (or even more) engineering effort overall.

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 that the existing highly social construct of informal mathematical proof will remain intact, just with humans replaced by agents, but amongst mathematicians there is a growing realization that formalization is the best way to deal with this epistemological crisis.

It helps that work done in Lean (on Mathlib and other developments) is reaching an inflection point just as these questions become practically relevant from AI.

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 interactive theorem provers since before I was ever a professional software engineer, so it’s a bit of a dream come true to be able to pursue this full-time.

The example in this blurb is a pretty good one: https://www.hboehm.info/c++mm/why_undef.html

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.

According to the linked proposal, these implicit capability parameters are lexically bound, not dynamically bound.

> 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.

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.

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), which has more obviously Slavic elements.

The standard historical explanation for this is that Yiddish began as a Germanic language, and the Eastern dialects developed after Jews were expelled from Germany in the 14th century and migrated East. There were already Jews living there, but the population grew tremendously with the migration.

Paul Wexler's thesis is that the Eastern dialects of Yiddish actually independently descend from early Jewish Slavic languages (e.g. https://en.wikipedia.org/wiki/Knaanic_language), and the Western dialects are derived from the Eastern ones.

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?

> 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.

Arguably, Homotopy type theory still doesn't solve the problem, because while it strengthens the consequences of isomorphism it doesn't distinguish between "isomorphism" and "canonical isomorphism", whereas (some?) mathematicians informally seem to think that there's a meaningful difference.

> The only problem is that the author is working in Lean and apparently* dismissive of non-classical type theory. So now we're back to lamenting that equality in type theory is broken...

In my opinion, Lean made a number pragmatic choices (impredicative Prop, non-classical logic including the axiom of global choice, uniqueness of identity proofs, etc.) that enable the practical formalization of mathematics as actually done by the vast majority of mathematicians who don't research logic, type theory, or category theory.

It's far from established that this is possible at all with homotopy type theory, yet alone whether it would actually be easier or more economical to do so. And even if this state of affairs is permanent, homotopy type theory itself would still be an interesting topic of study like any other field of mathematics.

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 many irregularities that could only come out of a standards process, there are too many compiler bugs (just try using header units), the different implementations are too fragmented (I’m only using clang, which makes this easier on me), and there is a lack of things like module maps that would dramatically improve usability.

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 existing proofs with a large computational element handled by untrusted software, but I think this is the first one where the epistemological status of the result was uncertain in the larger mathematical community.

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.

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 this case, I personally wish the language had support for it, since it would allow you to seamlessly refactor a piece of code into its own function.

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.

> (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 is actually that they are more efficient as separate passes operating on packed data structures rather than e.g. a parser that calls into a lexer for each individual token. In a way, this is a claim that Wirth’s approach is inherently inefficient on contemporary CPU microarchitectures.

> Mathjax, mathml and stuff are less than 10 years old

MathML is from the 90s and MathJax is from 2009.

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 steam:

https://github.com/rust-lang/rfcs/issues/391

Intuitively, the bottom lifetime should the one that is uninhabited, which would be a lifetime with no extent rather than 'static.

`static is actually the superlifetime of all lifetimes, but & is contravariant in its lifetime parameter (and covariant in its type parameter).

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 works.

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.

> 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.

> 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 it.

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 are several aspects of the current Rust language that were effectively defined by arbitrary decisions made by the implementors, which aren't really spelled out anywhere besides the code.

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).