←back to thread

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

(www.youtube.com)
1479 points sandslash | 2 comments | 19 Jun 25 00:33 UTC | HN request time: 0.589s | source
Show context
practal ◴[19 Jun 25 04:42 UTC] 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. lelanthran ◴[19 Jun 25 16:50 UTC] No.44320353[source]▶
> 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.

That sounds like a paradox.

Formal verification can prove that constraints are held. English cannot. mapping between them necessarily requires disambiguation. How would you construct such a disambiguation algorithm which must, by its nature, be deterministic?

replies(1): >>44324574 #
2. practal ◴[20 Jun 25 03:52 UTC] No.44324574[source]▶
Going from informal to formal can be done using autoformalization [1]. The real question is, how do you judge that the result is correct?

[1] Autoformalization with Large Language Models — https://papers.nips.cc/paper_files/paper/2022/hash/d0c6bc641...