enum

Right. And the arguably simpler problem, where the model gets the C code directly, is active research: https://www.darpa.mil/research/programs/translating-all-c-to...

All of this work is extraordinarily impressive. It is hard to predict the impact of any single research project the week it is released. I doubt we'll ever throw away GCC/LLVM. But, I'd be surprised if the Claude C Compiler didn't have long-term impact on computing down the road.

This is a conjecture: modern chips are optimized to make the output code style of GCC/Clang go fast. So, the compilers optimize for the chip, and the chip optimizes for the popular compilers.

It’s in Rust…

Nice article. I believe the Claude C Compiler is an extraordinary research result.

The article is clear about its limitations. The code README opens by saying “don’t use this” which no research paper I know is honest enough to say.

As for hype, it’s less hyped than most university press releases. Of course since it’s Anthropic, it gets more attention than university press.

I think the people most excited are getting ahead of themselves. People who aren’t impressed should remember that there is no C compiler written in Rust for it to have memorized. But, this is going to open up a bunch of new and weird research directions like this blog post is beginning to do.

This isn't true right? You really can bring in zero dollars in grants and phone it in in the classroom. (Now, literally on Zoom!) I don't think it helps to pretend that everyone keeps pushing hard post tenure.

But, I think most people do. The system is deliberately designed to push an assistant professor so hard, that when they get a permanent contract, they're conditioned to keep pushing. It typically succeeds.

For tenure-track professors at top-twenty schools, step five is hard. Their tenured professors jealously guard their status, so rejection is the default. However, as school ranking goes down, runaway nepotism swiftly supplants professorial pride. At schools ranked worse than fifty, acceptance is the default.

Like everyone else, I have always had the pleasure of being at a top-20 school (in some list or the other!). Fortunately, I think this article is only attacking tenure at schools rated lower. (Let me know if I misinterpreted the article.)

We could eliminate tenure at lower-ranked schools. I'm not sure who will teach there if we do. The 90th percentile salary for a new tenure-track professor is 145K (https://cra.org/wp-content/uploads/2024/05/2023-CRA-Taulbee-... page 49). Nobody competent is going to take that salary without the possibility of tenure.

I just have an unprivileged secondary local account and do ssh dummy@localhost.

Is this wrong?

This was vibe coded in a few hours with Codex 5.2 Medium. We now have examples of agent-written web browsers and Unix-y OSes (https://github.com/viralcode/vib-OS). I thought it would be interesting to try something a little more out of distribution. All done in a single Codex session -- transcript is part of the release.

Thanks. As I said, I have no idea. :)

I'm not sure this is true. Encoding theorems in dependent types takes a lot of expertise.

Even without the Lean technical details, a lot of math theorems just don't mean anything to most people. For example, I have no idea what the Navier-Stokes theorem is saying. So, I would not be able to tell you if a Lean encoding of the theorem is correct. (Unless of course, it is trivially broken, since as assuming False.)

The worst case is that you vibe code a theorem that reads:

False => P

Then you vibe code a proof of this theorem. Then you get excited that you’ve proven P.

Some of the X discussion that prompted the OP was quite close to this. There are screenshots on X of Lean code that doesn’t compile, with Lean being blamed.

The post says this in other words: in Lean, Rocq, or any other theorem prover, you get a formally-verified proof, but you do NOT get a formally verified theorem statement.

So, even if the proof is correct, you need to determine if the theorem is what you want. Making that determination requires expertise. Since you cannot "run the theorem", you cannot vibe-code your way through it. E.g., there is no equivalent of "web app seems to be working!" You have to actually understand what the theorems are saying in a deep way.

Referring to this: https://github.com/arjunguha/slopcoder

I then proceeded to use it to hack on its own codebase, and close a bunch of issues in a repository that I maintain (https://github.com/nuprl/MultiPL-E/commits/main/).

I'm trying to determine what programming tasks are not in this list. :) I think it is trying to exclude adding new features and fixing bugs in existing code. I've done enough of that with LLMs, though not in large codebases.

I should say I'm hardly ever vibe-coding, unlike the original article. If I think I want code that will last, I'll steer the models in ways that lean on years of non-LLM experience. E.g., I'll reject results that might work if they violate my taste in code.

It also helps that I can read code very fast. I estimate I can read code 100x faster than most students. I'm not sure there is any way to teach that other than the old-fashioned way, which involves reading (and writing) a lot of code.

I don't think I can scientifically compare the agents. As it is, you can use Opus / Codex in Cursor. The speed of Cursor composer-1 is phenomenal -- you can use it interactively for many tasks. There are also tasks that are not easier to describe in English, but you can tab through them.

I teach at a university, and spend plenty of time programming for research and for fun. Like many others, I spent some time on the holidays trying to push the current generation of Cursor, Claude Code, and Codex as far as I could. (They're all very good.)

I had an idea for something that I wanted, and in five scattered hours, I got it good enough to use. I'm thinking about it in a few different ways:

1. I estimate I could have done it without AI with 2 weeks full-time effort. (Full-time defined as >> 40 hours / week.)

2. I have too many other things to do that are purportedly more important that programming. I really can't dedicate to two weeks full-time to a "nice to have" project. So, without AI, I wouldn't have done it at all.

3. I could hire someone to do it for me. At the university, those are students. From experience with lots of advising, a top-tier undergraduate student could have achieved the same thing, had they worked full tilt for a semester (before LLMs). This of course assumes that I'm meeting them every week.

- https://publish.obsidian.md/aixplore/Practical+Applications/...

   Does it work if you change to torch.bfloat16?

  The PyTorch 2.9 wheels do work. You can pip install torch --index-url <whatever-it-is> and it just works. You do need to build flash attention from source, which takes an hour or so.

I think that personal computing is more fun than time-shared computing. :)

It's remarkable what can now be done on a whisper-quiet little box. I hope the Strix Halo's will be just as much fun, and they should be, so long as Flash Attention works.

I’m not complaining. The clusters are great. The non-Slurm H100s are great. The Spark is more fun.

+1

I have H100s to myself, and access to more GPUs than I know what to do with in national clusters.

The Spark is much more fun. And I’m more productive. With two of them, you can debug shallow NCCL/MPI problems before hitting a real cluster. I sincerely love Slurm, but nothing like a personal computer.

I learned a lot from implementing this book. Compiler was in OCaml. Runtime was in C (used as a glorified assembly).

SGTM. The transparency is good.

Lots of discussion about choice of programming language in the comments below.

- In principle, it should not matter at all, but there are practical reasons why one PL may be better than another in a particular school or context.

- But, all this "choice of PL" discussion is really a discussion about CS1. A CS degree has at least seven other courses -- assuming 1 CS course per semester -- and in practice many more than that. So, if you're going to ask questions about CS1, the question to ask is, "Does CS1 setup students to succeed in the advanced courses?" Classically, these were courses in compilers, operating systems, networking, and so on. These days, you can add distributed computing, machine learning, etc. (but don't subtract the classics).

Things like this: https://arstechnica.com/tech-policy/2025/04/survey-americans...

I’m also quite sure letters matter for undergraduate admissions. They certainly do at the graduate level.

I think the average American today, including the average admissions officer, has a negative view of technology. So, an application that is unequivocally optimistic about technology is unlikely to be well received. I think that that is what happened here. We also have no visibility into letters of recommendation, which are likely a big factor.

What a PhD student hopefully gets from an advisor is more targeted advice than the type of boilerplate generic advice in this article and others like it.

An advisor who knows what the student wants to accomplish, and is capable of accomplishing should be able to determine when building a working system is more valuable than pushing yet another paper, when reforming science in a small way is likely succeed, and so on.

Sure. Thats not the goal here. These problems are hard for humans and (mostly) hard for LLMs.

It’s not that the benchmark is hard, but that the reasoning models do so much better than the non-reasoning models. That suggests it is testing a capability that reasoning models have that non-reasoning models do not.

Getting to 100% may require tokenization innovation, sure.

The problems are not important, but they illustrate failures that are. For example:

- The paper has an example where the model reasons "I'm frustrated" and then produces an answer that it "knows is wrong". You wouldn't know it if you didn't examine the reasoning tokens.

- There are two examples were R1 often gets stuck "thinking forever"

If these failures happen on these questions, where else can happen? We'll start to find out soon enough.

Heuristic search, not exhaustive search, is an essential ingredient of reasoning. Has been true since chess. Remains true with MCTS, LLMs, etc.