Worth pointing out a success story: all ACM publications have gone open access starting this year[1]. Papers are now going to be CC licensed, with either the very open CC-BY[2] license or the pretty restrictive (but still better than nothing!) CC-BY-NC-ND[3] license.

Computer science as a discipline has always been relatively open and has had its own norms on publication that are different from most other fields (the top venues are almost always conferences rather than journals, and turn-around times on publications are relatively short), so it isn't a surprise that CS is one of the first areas to embrace open access.

Still, having a single example of how this approach works and how grass-roots efforts by CS researchers led to change in the community is useful to demonstrate that this idea is viable, and to motivate other research communities to follow suit.

[1]: https://authors.acm.org/open-access/acm-open-for-authors-hom...

[2]: https://creativecommons.org/licenses/by/4.0/

[3]: https://creativecommons.org/licenses/by-nc-nd/4.0/deed.en

> you can't spec out something you have no clue how to build

Ideally—and at least somewhat in practice—a specification language is as much a tool for design as it is for correctness. Writing the specification lets you explore the design space of your problem quickly with feedback from the specification language itself, even before you get to implementing anything. A high-level spec lets you pin down which properties of the system actually matter, automatically finds an inconsistencies and forces you to resolve them explicitly. (This is especially important for using AI because an AI model will silently resolve inconsistencies in ways that don't always make sense but are also easy to miss!)

Then, when you do start implementing the system and inevitably find issues you missed, the specification language gives you a clear place to update your design to match your understanding. You get a concrete artifact that captures your understanding of the problem and the solution, and you can use that to keep the overall complexity of the system from getting beyond practical human comprehension.

A key insight is that formal specification absolutely does not have to be a totally up-front tool. If anything, it's a tool that makes iterating on the design of the system easier.

Traditionally, formal specification have been hard to use as design tools partly because of incidental complexity in the spec systems themselves, but mostly because of the overhead needed to not only implement the spec but also maintain a connection between the spec and the implementation. The tools that have been practical outside of specific niches are the ones that solve this connection problem. Type systems are a lightweight sort of formal verification, and the reason they took off more than other approaches is that typechecking automatically maintains the connection between the types and the rest of the code.

LLMs help smooth out the learning curve for using specification languages, and make it much easier to generate and check that implementations match the spec. There are still a lot of rough edges to work out but, to me, this absolutely seems to be the most promising direction for AI-supported system design and development in the future.

3- Anthropic looks "woke" and the administration cares more about perceptions than reality.

Not too different from picking on Harvard/etc.

I mean, look at all the startups that succeeded despite being complete shitshows behind the scenes... the baseline for leadership, organization, coordination or, hell, execution for a startup to succeed isn't exactly high either.

Living with ADHD also increases your chances of getting into a car accident substantially. I can't find the numbers now, but the increase is non-trivial and there are some clear mechanisms (inattention, impulsivity and risk-seeking behaviors).

ADHD is a big part of the reason I don't drive. I'm lucky enough to live in Berkeley which is very walkable with decent transit, and I would hesitate to move anywhere more car-oriented exactly because I have ADHD.