lacker

What jumped out at me is that the author had three internships. Those are essentially "entry-level positions". If you do well at an internship, you typically get a job offer. If you don't do well, usually you can at least get some useful feedback.

I'm not saying that everything is perfectly fine in the job market right now, it's just a lot more productive to focus on "what skill do I need to work on, that would have let me convert those internships into full time jobs", rather than "man the job market is bad".

I personally like AI but it has definitely shifted my job. There is less "writing code", more "reviewing code", and more "writing sentences in English". I can understand people being frustrated.

To me it's like a halfway step toward management. When you start being a manager, you also start writing less code and having a lot more conversations.

The point I found most interesting is what the author calls "robustness".

Another advantage of AlphaEvolve was robustness: it was relatively easy to set up AlphaEvolve to work on a broad array of problems, without extensive need to call on domain knowledge of the specific task in order to tune hyperparameters.

In software world "robustness" usually implies "resistance to failures", so I would call this something different, more like "ease of integration". There are many problems where in theory a pre-LLM AI could do it, but you would have to implement all this explicit modeling, and that's too much work.

Like to pick a random problem, why does no superhuman AI exist for most video games? I think most of the difficulty is not necessarily in the AI algorithm, it's that the traditional method of game playing involves programming a model of the game, and for most video games that's an incredible amount of work, too much for someone to do in their spare time.

LLMs, on the other hand, are decent at integrating with many different sorts of systems, because they can just interoperate with text. Not quite good enough at video yet for "any video game" to fall. But a lot of these problems where the difficulty is not "algorithmic" but "integration", the LLM strategy seems promising for cracking.

Batteries are also a pretty good solution. It's possible that eventually there is enough battery storage on the grid that we can shut down the highest-risk transmission lines for longer periods of time without having power outages.

Casey Handmer has some interesting writing for people who are curious about this direction: https://caseyhandmer.wordpress.com/2023/07/12/grid-storage-b...

The nice thing about batteries is that they get cheaper and cheaper over time, as opposed to generic construction in California, which seems to get more and more expensive over time.

In my Mazda the wired CarPlay also seems to fail a lot. But whenever I rent a car with wireless CarPlay it's been fine. Take this one anecdote for what it's worth.

CarPlay has its pros and cons. I drive a Mazda and have rented enough GM and Ford vehicles to say that all of their software is consistently terrible. It's like every rectangle on the screen is built by a different team, all of whom hate each other. Different fonts, different modes of interaction, buttons that do nothing, error messages that complain about other parts of the software. So CarPlay is much better than any of those.

But at the same time I don't really use CarPlay for all that much. Music, maps, that's about it. And I also want to use the screen for some features that CarPlay doesn't handle, like checking backup or side cameras. In theory you could do even more, like if I have some engine problem why does it alert me with a few words in a tiny amount of UI in some random spot? It could give me a full explanation of what's going wrong, tell me whether it's in warranty, and offer me to schedule an appointment, right there from the screen in my car.

I haven't driven a Tesla or a Rivian so I don't know how good their software is. But it does seem like there's an opportunity to build some actually-good software here that a generic platform like CarPlay can't really do.

Yeah, I just meant proposition-as-types. Sloppy terminology by me. I meant to complain about the general conflation of the "proving system" and the "typechecking system".

Generally in dependent type systems you are limited in some way in what sort of values a type can refer to. The fancy type checking happens at compile time, and then at run time some or most of the type information is erased. The implementation is tricky but the more difficult problem IMO is the developer experience; it involves a lot of extra work to express dependent types and help the compiler verify them.

That's a good point, for example in Eigen you can do

Eigen::Matrix<float, 10, 5>

I just really want it in Python because that's where I do most of my matrix manipulation nowadays. I guess you also would really like it to handle non-constants. It would be nice if these complicated library functions like

torch.nn.MultiheadAttention(embed_dim, num_heads, dropout=0.0, bias=True, add_bias_kv=False, add_zero_attn=False, kdim=None, vdim=None, batch_first=False, device=None, dtype=None)

would actually typecheck that kdim and vdim are correct, and ensure that I correctly pass a K x V matrix and not a V x K one.

Dependent types are very useful for some things. For example, I wish Python had the ability to express "a 10 x 5 matrix of float32s" as a type, and typecheck that.

The Curry-Howard correspondence, using dependent type system to have "proofs" be equivalent to "types", is powerful, but it can be really confusing. From a human point of view, there is a huge difference between "Your proof is wrong" and "You wrote a statement that fails typechecking".

Intuitively, when you make an error with types, it should be something fairly trivial that you just read the error and fix it up. When you make an error in a proof, it's understandable if it's very complicated and requires thought to fix. The natural UI is different.

So I agree with the author that the greatest benefit of Lean is not its typesystem per se, but its community. Specifically the fact that Lean's library of mathematics, mathlib, is organized like an open source community with pull requests. Whereas Isabelle's library of mathematics, the AFP, is organized like a scientific journal with referees.

I'm working on a dependent type system at the moment for a new theorem prover - Acorn, at https://acornprover.org - and my hope is to combine the good points of both Lean and Isabelle. It's nice that Lean has the power to cleanly express the simple dependent types that mathematicians often use, like vector spaces or quotients. But if you use dependent types too much then it does get complicated to debug what's happening.

The only thing I dreaded more was trying to run other people's C++ projects.

It's like the negativity whenever a post talks about hiring or firing. A lot of people are afraid that they are going to lose their jobs to AI.

For anyone that's interested in formalizing mathematics but wished there was an easier way to do it, I've been working on a different sort of theorem prover recently.

https://acornprover.org

The idea is that there's a small AI built into the VS Code extension that will fill in the details of proofs for you. Check it out if you're interested in this sort of thing!

I whitelisted github.com, api.github.com, *.github.com, and it still doesn't seem to work. I suspect they did something specifically for github to prevent the agent from doing dangerous things with your credentials? But I could be wrong.

The sandbox idea seems nice, it's just a question of how annoying it is in practice. For example the "Claude Code on the web" sandbox appears to prevent you from loading `https://api.github.com/repos/.../releases/latest`. Presumably that's to prevent you from doing dangerous GitHub API operations with escalated privileges, which is good, but it's currently breaking some of my setup scripts....

They're renaming Coq, too, for the obvious reason.

Just go ahead and rename this project to "Rocuda", save everyone a lot of time arguing about what names are appropriate or not.

Personally, I'm not religious. But 20% of Americans believe that the Bible is the literal word of God. Is it really so crazy for one venture capitalist to believe that the Antichrist is real?

Part of the freedom of religion is accepting that other Americans really do have religious beliefs that differ from your own sometimes, and that's okay. It doesn't mean you need to support the policies that he supports. But we do need to share this country peacefully with people who don't have the same religious beliefs that we do.

It is not a sin to hire people when you aren't 100% confident your business is going to succeed. That's just how startups work.

Some people are not in a position in their life to take any risk of losing their job, and that's perfectly understandable, but those people should not take a job at a startup.

> Sam is spinning the world on his finger tip with these deals he's crafting.

That was my reaction too, this sort of weird deal seems very Sam Altman style.

Like Elon Musk - ironically, the archenemies are very stylistically similar.

Type hints are much easier to use nowadays than they were a few years ago, because the agentic tools like Claude Code are very good at converting an existing codebase to using type hints.

We DID build good transit. It takes 15 minutes to get from the MacArthur BART to downtown San Francisco! But the walkable area around that station is full of single-family housing. It's a huge waste building all of this incredible public transit and then not allowing apartment buildings near it.

The same is true for so many of the East Bay BART stops. Amazing transit but apartment buildings are banned so it's much more expensive to live there than it should be.

A big question is whether these areas actually turn into denser housing, or whether something else in the process manages to bog it down. Plenty of housing bills have seemed like a big deal when you looked at the area they impacted, but in practice they led to little new housing.

Of course a crime-fighting company "sells to police forces and corporations". Who else would you sell crime-fighting tools to?

Flock reminds me of Replit: they both predate the modern era of AI, and in some sense they were lucky to be well-positioned when advances in AI enabled their core product to become much more powerful. Of course, the harder you work, the luckier you get....

I'm confused, I feel like the two of you are expressing opposite opinions.

The comment you are responding to prefers green threads to be managed like goroutines, where the code looks synchronous, but really it's cooperative multitasking managed by the runtime, to explicit async/await.

But then you criticize "code that looks synchronous but is really async". So you prefer the explicit "async" keywords? What exactly is your preferred model here?

I think LLMs are different because they are such a powerful developer technology. The most powerful I have seen in 25 years.

Some engineers went from useful to useless almost overnight. Someone who is stubbornly stuck in their ways and refuses to use AI tools, and yet spends days failing to achieve what Claude Code can do in a few requests, well... what's going to happen to them? All of a sudden there's no work they can do, because the easy problems got solved by the AI.

So it ends up being the manager's job, either find something that this person can do, train them up to use modern technology, or fire them.

It sounds better than the northern California system where occasionally PG&E will cut off the power of random neighborhoods because the grid is overloaded.

This claim from the article is too extreme: "It is safe to say that prior to 1610 not a single significant scientific argument had turned on a question of fact."

Just in astronomy alone, in the previous century Tycho Brahe was debating against the Copernican models, with his own hybrid model where most of the planets orbit the sun, but the sun orbits the earth. Facts about which model predicted the location of what planets were really important.

The book "The Copernican Revolution" by Kuhn is really interesting for anyone curious to know more about this period.

In my experience the FAANG companies don't really abuse their H-1Bs. At Google or Meta the H-1Bs really are just smart people who participate as full and equal peers. And the FAANGs employ plenty of American citizens, they hire all the good employees they can get. The trouble either comes from small companies or from consulting shops.

The simplest solution is just to take salary into account. If someone is making $180k a year then they aren't "owned".

By the time they are hoping to finish in 2029, I bet LLMs are capable of translating the proof from Lean into the alternate theorem proving language of your choice with only a small amount of human assistance.

If this does end up being the case, that translation becomes easy, then essentially all theorem proving efforts should be conducted in the language that is the easiest to work in. You can translate into the "mathematically superior" languages later.

Draw 99 circles in a row, then draw a separate polygon around each one with only a teeny amount of excess area, then connect those polygons with teeny little connectors to make it a single polygon. When I say "teeny", you can make those arbitrarily small, so you can certainly fit them under 1 total area.

Okay, it's maybe not "obvious" in a regular human sense, but in a graduate math class you could claim this was "obvious". It would be pretty clear if I were drawing a diagram on a whiteboard. I would definitely take less time proving this to a human, than formalizing it.

Typically formalization is actually harder than solving a problem. You almost always solve before formalizing. And it can be surprisingly hard to formalize problems that are easy to solve.

For example, is there a polygon of area 100 that you can fit 99 circles of area 1 inside it, without overlapping? Yes, obviously, it's very easy to prove this informally. Now try formalizing it! You will find it takes a while to formalize a number of fairly obvious geometric statements.