4 ms·

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 rea

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.

sargstuff 3y ago
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.
- schoen 3y ago
  Adding a large language model is going to move you in the exact opposite direction from ease of formal verification.
  - epgui 3y ago
    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.
    - schoen 3y ago
      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!
      - ratmice 3y ago
        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.
mostlylurks 3y ago
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.
Jaxan 3y ago
My feeling is that proof assistants are much closer to general purpose programming than logic programming such as prolog.

sargstuff 3y ago

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.

schoen 3y ago
Adding a large language model is going to move you in the exact opposite direction from ease of formal verification.
- epgui 3y ago
  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.
  - schoen 3y ago
    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!
    - ratmice 3y ago
      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.

mostlylurks 3y ago

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.

Jaxan 3y ago

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