Live data from Hacker News

Andrej Karpathy: Software in the era of AI [video]

youtube.com

581–590 of 827 posts

Re: Andrej Karpathy: Software in the era of AI [video]

#581
post #50

Great talk, thanks for putting it online so quickly. I liked the idea of making the generation / verification loop go brrr, and one way to do this is to make verification not just a human task, but a machine task, where possible. Yes, I am talking about formal verification, of course! That also goes nicely together with "keeping the AI on a tight leash". It seems to clash though with "English is the new programming l…

> "English is the new programming language."

For those who missed it, here's the viral tweet by Karpathy himself: https://x.com/karpathy/status/1617979122625712128

Re: Andrej Karpathy: Software in the era of AI [video]

#582

Earlier quoted context omitted.

Why? Why would the language used to express proof of correctness have anything to do with English? English was not developed to facilitate exact and formal reasoning. In natural language ambiguity is a feature, in formal languages it is unwanted. Just look at maths. The reasons for all the symbols is not only brevity but also precision. (I dont think the symbolism of mathematics is something to strive for though, we…

My answer is already in my previous comment: if you have two formal languages to choose from, you want the one closer to natural language, because it will be easier to see if informal and formal statements match. Once you are in formal land, you can do transformations to other formal systems as you like, as these can be machine-verified. Does that make sense?

Not really. You want the one more aligned to the domain. Think music notation. Languages have more evolved to match abstractions that help with software engineering principles than to help with layman understanding. (take SQL and the relational model, they have more relation with each other than the former with natural languages)

Re: Andrej Karpathy: Software in the era of AI [video]

#583

Earlier quoted context omitted.

You would definitely think so, Lean is in a great position here! I am betting though that type theory is not the right logic for this, and that Lean can be leapfrogged.

Why? By the completeness theorem, shouldn't first order logic already be sufficient? The calculus of constructions and other approaches are already available and proven. I'm not sure why we'd need a special logic for LLMs unless said logic somehow accounts for their inherently stochastic tendencies.

Completeness for FOL specifically says that semantic implications (in the language of FOL) have syntactic proofs. There are many concepts that are inexpressible in FOL (for example, the class of all graphs which contain a cycle).

Re: Andrej Karpathy: Software in the era of AI [video]

#584
post #374

Earlier quoted context omitted.

If "AI" worked (which fortunately isn't the case), humans would be degraded to passive consumers in the last domain in which they were active creators: thinking. Moreover, you would have to pay centralized corporations that stole all of humanity's intellectual output for engaging in your profession. That is terrifying. The current reality is also terrifying: Mediocre developers are enabled to have a 10x volume (not q…

> If "AI" worked (which fortunately isn't the case), humans would be degraded to passive consumers in the last domain in which they were active creators: thinking. "AI" (depending on what you understand that to be) is already "working" for many, including myself. I've basically stopped using Google because of it. > humans would be degraded to passive consumers in the last domain in which they were active creators: th…

The AI as it is currently, will not come up with that new app idea or that clever innovative way of implementing an application. It will endlessly rehash the training data it has ingested. Sure, you can tell an AI to spit out a CRUD, and maybe it will even eventually work in some sane way, but that's not innovative and not necessarily a good software. It is blindly copying existing approaches to implement something. That something is then maybe even working, but lacks any special sauce to make it special.

Example: I am currently building a web app. My goal is to keep it entirely static, traditional template rendering, just using the web as a GUI framework. If I had just told the AI to build this, it would have thrown tons of JS at the problem, because that is what the mainstream does these days, and what it mostly saw as training data. Then my back button would most likely no longer work, I would not be able to use bookmarks properly, it would not automatically have an API as powerful as the web UI, usable from any script, and the whole thing would have gone to shit.

If the AI tools were as good as I am at what I am doing, and I relied upon that, then I would not have spent time trying to think of the principles of my app, as I did when coming up with it myself. As it is now, the AI would not even have managed to prevent duplicate results from showing up in the UI, because I had a GPT4 session about how to prevent that, and none of the suggested AI answers worked and in the end I did what I thought I might have to do when I first discovered the issue.

Re: Andrej Karpathy: Software in the era of AI [video]

#585

Earlier quoted context omitted.

This is why I call all this AI stuff BS. Using a formal language is a feature, not a bug. It is a cornerstone of all human engineering and scientific activity and is the _reason_ why these disciplines are successful. What you are describing (ie. ditching formal and using natural language) is moving humanity back towards magical thinking, shamanism and witchcraft.

> What you are describing (ie. ditching formal and using natural language) is moving humanity back towards magical thinking ... "Any sufficiently advanced technology is indistinguishable from magic."

indistinguishable from magic != magic

Re: Andrej Karpathy: Software in the era of AI [video]

#586

I spent a lot of time thinking about this recently. Ultimately, English is not a clean, deterministic abstraction layer. This isn't to say that LLMs aren't useful, and can create some great efficiencies.

no, but a subset of English could be

Let me introduce to you.. python ;)

Re: Andrej Karpathy: Software in the era of AI [video]

#587

Software 3.0 is the code generated by the machine, not the prompts that generated it. The prompts don't even yield the same output; there is randomness. The new software world is the massive amount of code that will be burped out by these agents, and it should quickly dwarf the human output.

Code is read much more often than it is written. Code generated by the machine today will be prompt read by the machine going forward. It's a closed loop.

Software is a world in motion. Software 1.0 was animated by developers pushing it around. Software 3.0 is additionally animated by AI agents.

Re: Andrej Karpathy: Software in the era of AI [video]

#588
post #50

Great talk, thanks for putting it online so quickly. I liked the idea of making the generation / verification loop go brrr, and one way to do this is to make verification not just a human task, but a machine task, where possible. Yes, I am talking about formal verification, of course! That also goes nicely together with "keeping the AI on a tight leash". It seems to clash though with "English is the new programming l…

This thread perfectly captures what Karpathy was getting at. We're witnessing a fundamental shift where the interface to computing is changing from formal syntax to natural language. But you can see people struggling to let go of the formal foundations they've built their careers on.

Yep, that why I never write anything out using mathmatical expressions. Natural language only baby!

Re: Andrej Karpathy: Software in the era of AI [video]

#589
This DevOps friction is exactly why I'm building an open-source "Firebase for LLMs." The moment you want to add AI to an app, you're forced to build a backend just to securely proxy API calls—you can't expose LLM API keys client-side. So developers who could previously build entire apps backend-free suddenly need servers, key management, rate limiting, logging, deployment... all just to make a single OpenAI call. Anyone else hit this wall? The gap between "AI-first" and "backend-free" development feels very solvable.
Post reply on HN