Hacker News Reader

Comment by rabbits77 | Hacker News Reader

I can’t see why this should not be the case. Logic Programming languages like Prolog can be used for general purposes. The main catch is that you need to be really good at Prolog to use it to full generality. But if you’re willing to put in the time it should be able the same.

View on HN

Understanding the techniques that make general purpose programming in prolog easy is one of the easiest parts of learning prolog, such that even beginners shouldn't have trouble with it. Learning to use prolog the way it was meant to be used is actually much harder, and you'll certainly have a good grasp of general-purpose programming in prolog long before you become "really good" at prolog.

My feeling is that proof assistants are much closer to general purpose programming than logic programming such as prolog.

Just add a GPT natural language to language proof assistant translator as a front end (with appropriate audio device permissions)

Change the need to be really good at proglog to just need to distinctly describe what want/need.

Adding a large language model is going to move you in the exact opposite direction from ease of formal verification.

I mean... Not necessarily? It depends how you use it or what part of the process you delegate to it, no?

Whether AI produces Lean code or a human produces Lean code... The Lean code should speak for itself. Both humans and AI are the weak link in either case, and it's unclear to me which of the two is the weaker.

Oh, I think I misunderstood the proposal there. I thought the language model was meant to be producing (only) code, not proofs.

If it manages to produce successful proofs of pre-existing property specifications, then that's great!

Yeah, I think the catch is the "pre-existing property specifications" part. I think you need to carefully understand both AI & Human generated propositions. While proofs once checked are just gravy.

Reply on news.ycombinator.com