Could it be since a lot of the data is trained on captions? At least if I'm remembering correctly, that's what they use to create the association between what's seen and what's said.
I've heard this can be a bit of a pain in practice, is that true? I can imagine it could slow me down to construct a proof of an invariant every time I call a function (if I understand correctly).
I haven't worked significantly with lean but I'm toying with my own dependently typed language. generally you only have to construct a proof once, much like a type or function, and then you reuse it. Also, depending on the language there are rewriting semantics ("elaboration") that let you do mathematical transformations to make two statements equivalent and then reuse the standardized proof.
I feel like that's a rather bad-faith take, so if you're going to make that kind of accusation you better back it up. People can legitimately believe that AI is not going to be the end of the world, and also not be privileged. And people can be privileged, and also be right. Not everything can be reduced down into a couple of labels, and how those labels "always" interact.
Wasn't that the point of mentioning Jevon's Paradox though? Like they said in the essay, these things are quite elastic. There's always more demand for software then what can be met, so bringing down the cost of software will dramatically increase the demand for it. (Now, if you don't think there's a ton of demand for custom software, try going to any small business and ask them about how they do bookkeeping. You'll learn quite quickly that custom software would run much better than sticky notes and excel, but they can't afford a full time software developer as a small business. There's literally hundreds of thousands of places like this.)
Regardless of whether this means AGI has been achieved or not, I think this is really exciting since we could theoretically have agents look through papers and work on finding simpler solutions. The complexity of math is dizzying, so I think anything that can be done to simplify it would be amazing (I think of this essay[1]), especially if it frees up mathematicians' time to focus even more on the state of the art.
Maybe the best thing to say is we can only really forecast about 3 months out accurately, and the rest is wild speculation :)
History has a way of being surprisingly boring, so personally I'm not betting on the world order being transformed in five years, but I also have to take my own advice and take things a day at a time.
I will say one thing Claude does is it doesn't run a command until you approve it, and you can choose between a one-time approval and always allowing a command's pattern. I usually approve the simple commands like `zig build test`, since I'm not particularly worried about the test harness. I believe it also scopes file reading by default to the current directory.
I'm taking CS in college right now, and when we do our projects we're required to have a editor plugin that records every change made. That way when they grade it, they see how the code evolved over time, and not just the final product. Copying and posting has very distinct editor patterns, where organically developed code tends to morph over time.
I looked to see if BYU had made the source code available, but it doesn't look like they've published it. It's called code recorder, and before we do an assignment we have to enable recording. It generates a .json file that lists every single edit made in terms of a textual diff. They must have some sort of tool that reconstructs it when they grade. Sorry I don't know more!
Edit: I expect it wouldn't be super hard to create though, you'd just have to hook into the editor's change event, probably compute the diff to make sure you don't lose anything, and then append it to the end of the json.
I think it's fair for the projects, since when you first write code you're learning to think like a computer. Their AI policy is it's fine to ask it questions and have it explain concepts, but the project assignments need to be done without AI.
The one requirement I think is dumb though is we're not allowed to use the language's documentation for the final project, which makes no sense. Especially since my python is rusty.
Since you mentioned failure to figure out what better teaching methods are, I feel it's my sworn duty to put a plug for https://dynamicland.org and https://folk.computer, if you haven't heard about them :)
Yea, and I think it is amazing, but in the same time it will work for some and not for others
The same way scratch works for some, redstone for others, and https://strudel.cc/ for third
I think the truth is that we are more different than alike, and computers are quite strange.
I personally was professionally coding, and writing hundreds of lines of code per day for years, and now I look at this code and I can see that I was not just bad, I literally did not know what programming is.
Human code is an expression of the mind that thinks it. Some language allow us to better see into the author's mind, e.g forth and lisp, leak the most, c also leaks quite a lot e.g. reading antirez's code or https://justine.lol/lambda/, or phk or even k&r, go leaks the least I think.
Anyway, my point is, programming is quite personal, and many people have to find their own way.
PS: what I call programming is very distant from "professional software development"
I think one thing I've heard missing from discussions though is that each level of abstraction needs to be introspectable. LLMs get compared to compilers a lot, so I'd like to ask: what is the equivalent of dumping the tokens, AST, SSA, IR, optimization passes, and assembly?
That's where I find the analogy on thin ice, because somebody has to understand the layers and their transformations.
“Needs to be” is a strong claim. The skill of debugging complex problems by stepping through disassembly to find a compiler error is very specialized. Few can do it. Most applications don’t need that “introspection”. They need the “encapsulation” and faith that the lower layers work well 99.9+% of the time, and they need to know who to call when it fails.
I’m not saying generative AI meets this standard, but it’s different from what you’re saying.
Sorry, I should clarify: it's needs to be introspectable by somebody. Not every programmer needs to be able to introspect the lower layers, but that capability needs to exist.
Now I guess you can read the code an LLM generates, so maybe that layer does exist. But, that's why I don't like the idea of making a programming language for LLMs, by LLMs, that's inscrutable by humans. A lot of those intermediate layers in compilers are designed for humans, with only assembly generation being made for the CPU.
reply