Dragon-Hatcher

The language is Turing-complete, not the program. Rice's theorem says that we can't have a program that verifies a non-trivial property for all other programs. It doesn't say we can't verify that property for some programs. That would imply you could never know anything about a program.

I've read the FAQ (https://github.com/aallan/vera/blob/main/FAQ.md) that provides the justification for this and it is, IMO, fairly weak. The main argument is that misleading names can confuse models. I have no problem believing this bit I'm not sure why we should assume code will have misleading names. In fact, the same document says that in tests they've had LLMs mix up the indices, which is exactly the problem I would foresee. It seems especially messy that the name for the same variable will change in different places in the code. The utility of De Bruijn indices is easy substitutability of expressions, which seems like totally the wrong thing to optimize for in a programming language.

Edit: the more I think about it the more this seems like a really bad idea. Three more issues come to mind: 1) it becomes impossible to grep for a variable, which I know agents do all the time. 2) editing code at the top of the function, say introducing a new variable, can require editing all the code in the rest of the function, even if it was semantically unchanged! 3) they say it is less context for the LLM to track but now, instead of just having to know the name of one variable, you have to keep track of every other variable in the function

FIRST is a really amazing experience.

I just want to point out for those who don't do FTC how good they were. Here is a link to a summary of all their matches: https://ftcscout.org/teams/8405. Their top OPR (offensive power rating - a.k.a how many points they contributed per match) of 112 is really good. That puts them at 20th among teams who started this year out of nearly 1900 teams. (Although technically the team is older but it sounds like it had all new members.)

Here you can see all their events and how they ranked among all teams: https://ftcscout.org/records/2022/teams?filter=%7B%22all%22%...