3 ms·

I haven't looked much into this yet -- it seems very neat! -- but I wonder how hard it would be to create some kind of tactic language for this, akin to what th

I haven't looked much into this yet -- it seems very neat! -- but I wonder how hard it would be to create some kind of tactic language for this, akin to what the more conventional proof assistants like Coq, HOL, etc. have. If done minimalistically, it shouldn't blow up the project all that much, though ideally the system would be expandable with user-defined tactics. Not sure whether that tactic language would be inside the Formality language itself (like Coq does) or inside some already-existing language that is meta with respect to the Formality language (like HOL does). Having an already established language for that seems more convenient, but I'm not sure.

gnulinux 8y ago
Not pretending to be an expert but I did a lot of proofs in Agda (a related subject was my bachelor's thesis). In what way do you find tactics useful? I personally find Coq having bunch of mini-languages inside, one being a tactic language confusing. I think it's a non-optimal (though viable) solution to the problem. I think, as always, lisp gets it right. Computing is all about abstractions and sometimes even abstractions that can talk between each other and the best way to approach this problem is homoiconicity. I think agda gets it right, if you write macros helping you solve the problem at hand you can write very elegant and readable proofs. I understand that tactics are very popular in proof automation community and I'm very likely very wrong. But this is just a reflection of my experience. I'm currently writing my own dependently typed PL and am debating merits of tactics. So far I can't find a reason to add them provided you give enough lispness to your language.
- tomsmeding 8y ago
  My experience with this kind of stuff: done some Coq by myself and some HOL in class. Generally, the distinguishing feature of tactics is that they provide backward reasoning, instead of forward reasoning, what a verification engine would be written around. Mind that I haven't worked with any proof system yet besides Coq and HOL, so my opinion might be far out, but I think backward reasoning is a very nice way to construct proofs, especially in the context of a proof assistant. Aren't things like algorithms for simple automated proving more easily embedded in a tactic language than in a forward reasoning language? When reasoning backward, one naturally reduces the statement to prove to simpler and simpler statements, and at some point they become simple enough to be handled by some automatic prover. (auto/omega/... in Coq, PROVE_TAC/COOPER_TAC in HOL) When reasoning forward, I don't see how one would go about using automated provers like that, but it's likely I'm missing some idea here. > I'm currently writing my own dependently typed PL Awesome! I'm all for writing interesting new languages and implementations, especially in this area. Once you've got something to show, be sure to post here on HN, since people might enjoy looking around. :) (If it doesn't get lost in the swarm of submissions...)
  - gnulinux 8y ago
    I think forward reasoning works only because the underlying type theory is intuitive. When I approach proofs in agda, I simply approach it the same way I write haskell code. "You have bunch of cosets and you wanna go to group." You have objects (proofs) around and you want to construct an instance of a type (theorem) so you start with functions (lemmas) that give objects of desired types. Again, I'm not very familiar with Coq (only agda) but I suppose by backwards reasoning you mean the last unconstructed type in your proof is the type with highest level of abstraction. On the other hand, in agda it's the first one because either you already know a function (lemma) returning this type and need to construct it's arguments (assumptions) or you can use an anonymous function (implication introduction). This is a totally random and not a well-thought-out statement but to me it seems like the difference between agda and Coq seems like the difference between purely functional and imperative programming.
    - uryga 8y ago
      > the underlying type theory is intuitive isn't that "intuitionistic"?
      - gnulinux 8y ago
        No I meant intuitive like easy to understand for humans. (It is also intuitionistic but that's a technical fact shared by both Coq and Agda (though not HOL)). The reason I said that is because thinking in terms of types is very straightforward for people. "Give me a View and Serializer so I can give you JSON" "Why is my code not working? Oh because you can't always find the head of a list, I need to give you NonEmpty List T". Similarly, proving something is a group is like trying to go Group somehow from the objects around.
        uryga 8y ago
        ah, my bad, i see how that makes more sense. FWIW i agree – often, mentally converting a theorem to a type and thinking about the problem in that framework makes things easier for me to grasp. (also explains why we "apply" theorems/lemmas :) )
- fmap 8y ago
  Tactics are very useful when developing proofs rather than dependently typed programs (unless you are using very precise types, as is common in e.g. the Coq program package). The point is that in a proof you are usually not interested in the precise shape or computation behavior of the underlying proof term and this allows you to use far more aggressive automation than what you are doing with a typical macro. Likewise, you don't really want to see the proof term in the first place. Think about how long chains of equational reasoning are encoded in type theory - this is just noise that detracts from writing your proofs. As for homoiconicity, I think this is orthogonal to a tactic language. Both lean's tactics and template Coq allow you to reify the syntax of the type theory in order to write automation tactics, but this is separate from the proof search aspects of tactics.

gnulinux 8y ago

Not pretending to be an expert but I did a lot of proofs in Agda (a related subject was my bachelor's thesis). In what way do you find tactics useful? I personally find Coq having bunch of mini-languages inside, one being a tactic language confusing. I think it's a non-optimal (though viable) solution to the problem. I think, as always, lisp gets it right. Computing is all about abstractions and sometimes even abstractions that can talk between each other and the best way to approach this problem is homoiconicity. I think agda gets it right, if you write macros helping you solve the problem at hand you can write very elegant and readable proofs. I understand that tactics are very popular in proof automation community and I'm very likely very wrong. But this is just a reflection of my experience. I'm currently writing my own dependently typed PL and am debating merits of tactics. So far I can't find a reason to add them provided you give enough lispness to your language.

tomsmeding 8y ago
My experience with this kind of stuff: done some Coq by myself and some HOL in class. Generally, the distinguishing feature of tactics is that they provide backward reasoning, instead of forward reasoning, what a verification engine would be written around. Mind that I haven't worked with any proof system yet besides Coq and HOL, so my opinion might be far out, but I think backward reasoning is a very nice way to construct proofs, especially in the context of a proof assistant. Aren't things like algorithms for simple automated proving more easily embedded in a tactic language than in a forward reasoning language? When reasoning backward, one naturally reduces the statement to prove to simpler and simpler statements, and at some point they become simple enough to be handled by some automatic prover. (auto/omega/... in Coq, PROVE_TAC/COOPER_TAC in HOL) When reasoning forward, I don't see how one would go about using automated provers like that, but it's likely I'm missing some idea here. > I'm currently writing my own dependently typed PL Awesome! I'm all for writing interesting new languages and implementations, especially in this area. Once you've got something to show, be sure to post here on HN, since people might enjoy looking around. :) (If it doesn't get lost in the swarm of submissions...)
- gnulinux 8y ago
  I think forward reasoning works only because the underlying type theory is intuitive. When I approach proofs in agda, I simply approach it the same way I write haskell code. "You have bunch of cosets and you wanna go to group." You have objects (proofs) around and you want to construct an instance of a type (theorem) so you start with functions (lemmas) that give objects of desired types. Again, I'm not very familiar with Coq (only agda) but I suppose by backwards reasoning you mean the last unconstructed type in your proof is the type with highest level of abstraction. On the other hand, in agda it's the first one because either you already know a function (lemma) returning this type and need to construct it's arguments (assumptions) or you can use an anonymous function (implication introduction). This is a totally random and not a well-thought-out statement but to me it seems like the difference between agda and Coq seems like the difference between purely functional and imperative programming.
  - uryga 8y ago
    > the underlying type theory is intuitive isn't that "intuitionistic"?
    - gnulinux 8y ago
      No I meant intuitive like easy to understand for humans. (It is also intuitionistic but that's a technical fact shared by both Coq and Agda (though not HOL)). The reason I said that is because thinking in terms of types is very straightforward for people. "Give me a View and Serializer so I can give you JSON" "Why is my code not working? Oh because you can't always find the head of a list, I need to give you NonEmpty List T". Similarly, proving something is a group is like trying to go Group somehow from the objects around.
      - uryga 8y ago
        ah, my bad, i see how that makes more sense. FWIW i agree – often, mentally converting a theorem to a type and thinking about the problem in that framework makes things easier for me to grasp. (also explains why we "apply" theorems/lemmas :) )
fmap 8y ago
Tactics are very useful when developing proofs rather than dependently typed programs (unless you are using very precise types, as is common in e.g. the Coq program package). The point is that in a proof you are usually not interested in the precise shape or computation behavior of the underlying proof term and this allows you to use far more aggressive automation than what you are doing with a typical macro. Likewise, you don't really want to see the proof term in the first place. Think about how long chains of equational reasoning are encoded in type theory - this is just noise that detracts from writing your proofs. As for homoiconicity, I think this is orthogonal to a tactic language. Both lean's tactics and template Coq allow you to reify the syntax of the type theory in order to write automation tactics, but this is separate from the proof search aspects of tactics.