returningfory2

He has over quarter of a million subscribers so presumably it's his full time job?

Although now for all technical blog posts to HN I feel I should respond: such a weird way of flexing "I have a 6 figure tech job".

Maybe spell it out in more detail? Forgive my inability to follow the argument.

My overall point is that what's happening in SWE right now is not happening (yet?) in other fields. And so we can't extrapolate from SWE experience to wider social experiance.

I agree for SWE specifically that AI is changing the career dramatically, and in a way that makes life less predictable. But I don’t know how the definition of success has changed - at least in America it still seems to be good professional job plus family.

Right. Has that changed? Asking genuinely.

> we are living through a period of time where success is very hard to define, much less attain.

Do you think this has changed from say 10 or 20 years ago? To me, I don't get the sense that there has been shift in the social definition of success. Maybe I'm missing something?

> Does it count as a third space if you have to pay for it?

Yes, third spaces/places include places you need to pay for.

Thank you! I skimmed these citations and I remain unconvinced. But I think really answering the question would be a real research project, not a HN back and forth :)

The first citation's relevant highlight is "All categories of third places experienced widespread closures from 2019 to 2021" which is obviously a COVID phenomenon and not a cultural trend. They admit so much. Data from that period I would say is generally irrelevant to discussing wider cultural trends. In fact a query to Gemini says that the number of independent (not chain) coffee shops is growing at 3.2% across the country and it gives this citation: https://www.locationscloud.com/research-report/us-coffee-sho...

The other Science Direct article says "Third places _may_ be closing in neighborhoods across the United States" (my emphasis).

The remaining articles seem to be opinion articles without hard data. They focus on the hypothetical problem of third places going away. In fact the AEI article talks about zoning which cannot possibly be of relevance to any decline in third places given that zoning is becoming less restrictive over time in the last decade.

Is there a citation for the decline in third spaces? I read such a claim often. But in my part of the US (Brooklyn NY) the number of third spaces like coffee shops and pottery studios is booming.

Sorry to be a bit snarky, but I feel like the comment was kind of equivalent to calling me an idiot.

I'm sorry but this is _obviously_ not what I think. I _obviously_ don't think that merely typing a statement into Lean gives us a magic Lean proof. I am even aware that such a SuperLean is not even theoretically possible because of undecidability/halting problem/etc.

I have 3 VPSs so that I can run redundant copies of the data scraping software I wrote [0]. I've been scraping NYC subway data for 5+ years.

The biggest VPS hosts my NYC subway times app, my personal website, and other tools I build (most recently my pottery project management tool [1]).

Then in addition I've a bunch of monitoring software. I also run a rollouts system that automatically rolls out new versions of my projects when the GitHub CI builds them.

It's a really interesting thing to do! The maintenance is kind of the point: you get to learn essentially how to build a prod deployment.

[0] https://github.com/jamespfennell/hoard [1] https://log-demo.unionpots.nyc/

A tiny fraction compared to the proof, I'm guessing.

But the point is that you don't need to check the proof. But a lot of people seem to misunderstand what's happening and think you still need to check the Lean proof that AI outputs.

I feel this comment is based on a misunderstanding of how Lean works. In Lean you don't need to inspect the proof. There is no "closer inspection". All the human needs to verify is that the statement of the theorem is translated correctly from natural language to Lean. That usually covers a very small surface of the Lean code.

I wonder how Airbnb would respond to a host complaint that uses this data, because of the following story:

A few years ago me and a bunch of friends rented a big Airbnb with a no dogs policy. Some other friends were in the same town, with a dog, and came over and hung out in the yard for a while with their dog. The dog also briefly went in the house (which I think is poor form, to be clear). Somehow the Airbnb host was in the neighborhood and drove by the house to check on it, saw the dog, and then messaged Airbnb to complain.

My friend counter-complained to Airbnb that the host was surveilling us. And the end result was that Airbnb discounted the Airbnb by 50% (over $1000). The owner got nothing out of it. Very surprising to me.

Basically a similar technical disruption to what's happening in software engineering, but the implications are vastly different because the goals of software and math are not the same. For math, the disruption is leading to a deeper crisis of "what does it mean to be a mathematician?" Whereas for software "what does it mean to be a SWE?" hasn't really changed (the goal is to land software that does things for someone), rather the tooling has changed.

In more detail: in recent years there has been an effort to formalize mathematics using Lean and similar "theorem provers". You write your math proofs in a form of textual source code that Lean can verify for truth. But now Claude Code can produce source code to solve software problems (write me a tool that does X) and also produce source code to solve math (write me a Lean file that proves Y). Historically the main goal of math was to be solve big problems, but now Claude Code can do it. So what does a mathematician do?

Again, I think it's a more dire situation than for software because merely writing the code was never the full job. But for math writing the full proof kind of was.

This is a great observation. Options induce the worst kind of FOMO. People think: if only I had exercised I would now have $HUGE amount of shares. But the general counter-factual is that you exercise them and sell them pretty soon.

Agreed that this is why a lot of people support the current UB situation, but the history of UB makes this feel wrong:

> As far as I can tell, C89 did not use performance as a justification for any of its undefined behaviors. They were non-portabilities, like signed overflow and null pointer dereferences, or they were outright bugs, like use-after-free. But now experts like Chris Lattner and Hans Boehm point to optimization potential, not portability, as justification for undefined behaviors. I conclude that the rationales really have shifted from the mid-1980s to today: an idea that meant to capture non-portability has been preserved for performance, trumping concerns like correctness and debuggability.

https://research.swtch.com/ub

> People dont like any dating, they want to be past it into a long term healthy relationship mostly.

This is absolutely not true.

IIUC, the forgery path then involves getting any legitimate California license and changing the photo only? I guess that works.

Correct. In data protection, backup is not the feature. Restore is the feature.

This is a really good point.

Related, Matt Levine has recently been writing about how the AI labs are paying huge amounts of money to tech/math/AI people but these people don't actually know how to spend it. https://www.bloomberg.com/opinion/newsletters/2026-09-10/dal... As opposed to the typical finance worker who knows very well how to spend.

Yes, you need to manually verify the statement of the theorem of interest of formalized correctly. But you don't need to anything more than this: you can rely on the proof being correct. And the proof is overwhelmingly the most amount of code.

Yeah I think the verb "removed" is not the right verb here, because the paper in question is OpenAI's hypothetical paper which Alpöge is not on in the first place.

NYC zoning is less limiting than LA, but still extremely limiting.

I agree; that’s why I think we need a moratorium on human drivers while we figure this all out.

Awesome, thank you for sharing!

Very nice. As a follow up would be interesting to also reverse engineer the structure of the vtable itself. I guess it’s a list of pointers to the method implementations?

I think the issue is that you knew there was a bug to be found in the write and checkpoint interactions, which then determined which workload you built.

My understanding is that this workload is very uncommon: the Tailscale blog says they used a custom unusual configuration to have many checkpoints like this. So without knowing the bug, it seems unlikely one would build this workload and then find the bug. If that makes sense.

Edit: just want to say that you being able to repro it is awesome, but that the overall claim seems a little overstated to me.

Yep realized this after that my second solution (push a 0 if n is incremented) has the same branch prediction problem.

I think yours works. Alternatively in the loop:

    if out.len() < n {
        out.push(0);
    }
    out[n] = x;
    n += (x > threshold) as usize;

In this case the if will be predicted well because it only triggers log(N) times, given how the std lib extends vectors.

I disagree in the sense that you can rewrite the code to use the trick and also not allocate in advance. Nothing about the trick requires you to allocate up front: before writing to out[n] you can extend the vector if it’s out of bounds. Or, after incrementing n, do out.push(0).