←back to thread

1480 points sandslash | 3 comments | | HN request time: 0.67s | source
Show context
practal ◴[] No.44315505[source]
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 language". So the question is, can you hide the formal stuff under the hood, just like you can hide a calculator tool for arithmetic? Use informal English on the surface, while some of it is interpreted as a formal expression, put to work, and then reflected back in English? I think that is possible, if you have a formal language and logic that is flexible enough, and close enough to informal English.

Yes, I am talking about abstraction logic [1], of course :-)

So the goal would be to have English (German, ...) as the ONLY programming language, invisibly backed underneath by abstraction logic.

[1] http://abstractionlogic.com

replies(6): >>44315728 #>>44316008 #>>44319668 #>>44320353 #>>44322194 #>>44323749 #
1. redbell ◴[] No.44322194[source]
> "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

replies(1): >>44322614 #
2. throwaway314155 ◴[] No.44322614[source]
Referenced in the video of course. Not that everyone should watch a 40 minute long video before commenting but his reaction to the "meme" that vibe coding became when his tweet was intended as more of a shower thought is worth checking out.
replies(1): >>44326501 #
3. diggan ◴[] No.44326501[source]
> became when his tweet was intended as more of a shower thought

That was so obvious to me, and most of the people I talked to at the time, yet the ecosystem and media seems to have run with his "vibe-coding" idea as something people should implement in production yesterday, even though it wasn't meant as a "mantra" or even "here is where we should go"...