Most active commenters
  • practal(5)

←back to thread

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

(www.youtube.com)
1481 points sandslash | 11 comments | 19 Jun 25 00:33 UTC | HN request time: 1.568s | source | bottom
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. singularity2001 ◴[19 Jun 25 06:27 UTC] No.44316008[source]▶
lean 4/5 will be a rising star!
replies(1): >>44316452 #
2. practal ◴[19 Jun 25 07:54 UTC] No.44316452[source]▶
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.

replies(2): >>44316477 #>>44317553 #
3. gylterud ◴[19 Jun 25 08:02 UTC] No.44316477[source]▶
I think type theory is exactly right for this! Being so similar to programming languages, it can piggy back on the huge amount of training the LLMs have on source code.

I am not sure lean in part is the right language, there might be challengers rising (or old incumbents like Agda or Roq can find a boost). But type theory definitely has the most robust formal systems at the moment.

replies(1): >>44316688 #
4. practal ◴[19 Jun 25 08:46 UTC] No.44316688{3}[source]▶
> Being so similar to programming languages

I think it is more important to be close to English than to programming languages, because that is the critical part:

"As close to a programming language as necessary, as close to English as possible"

is the goal, in my opinion, without sacrificing constraints such as simplicity.

replies(1): >>44318644 #
5. voidhorse ◴[19 Jun 25 11:18 UTC] No.44317553[source]▶
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.

replies(2): >>44317774 #>>44322274 #
6. practal ◴[19 Jun 25 11:52 UTC] No.44317774{3}[source]▶
If first-order logic is already sufficient, why are most mature systems using a type theory? Because type theory is more ergonomic and practical than first-order logic. I just don't think that type theory is ergonomic and practical enough. That is not a special judgement with respect to LLMs, I want a better logic for myself as well. This has nothing to do with "stochastic tendencies". If it is easier to use for humans, it will be easier for LLMs as well.
7. gylterud ◴[19 Jun 25 13:45 UTC] No.44318644{4}[source]▶
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 can use sensible names in our languages, but the structure will need to be formal and specialised to the domain.)

I think there could be meaningful work done to render the statements of the results automatically into (a restricted subset of) English for ease of human verification that the results proven are actually the results one wanted. I know there has been work in this direction. This might be viable. But I think the actual language of expressing results and proofs would have to be specialised for precision. And there I think type theory has the upper hand.

replies(1): >>44319914 #
8. practal ◴[19 Jun 25 16:03 UTC] No.44319914{5}[source]▶
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?
replies(2): >>44322245 #>>44322727 #
9. skydhash ◴[19 Jun 25 20:27 UTC] No.44322245{6}[source]▶
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)
10. tylerhou ◴[19 Jun 25 20:32 UTC] No.44322274{3}[source]▶
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).
11. polivier ◴[19 Jun 25 21:33 UTC] No.44322727{6}[source]▶
> if you have two formal languages to choose from, you want the one closer to natural language

Given the choice I'd rather use Python than COBOL even though COBOL is closer to English than Python.