enum

The real question is how do you come up with a credible 3-5 year research program that is unlikely to be scooped or become pointless overnight.

3-5 years is the period of a grant, and grants have to make research progress, or you don’t get the next grant.

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.

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

Is this wrong?

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.