4 ms·

I've never seen a title that promised so much and delivered it all. That said, I'm very glad programming is not done through tactics. Editing proofs written wi

I've never seen a title that promised so much and delivered it all. That said, I'm very glad programming is not done through tactics. Editing proofs written with tactics is a nightmare - and the main reasons it's tolerated are the ubiquity of interactive provers and the fact that you basically don't care about which particular proof you get in a prover - unlike code, which rarely has interactive typechecking (Haskell holes come close) and where you do, definitely, care about the specific code you write. Using tactics for metaprogramming addresses all of those concerns, and it will be interesting to see if it picks up any kind of steam. Formalising the existing use of Eclipse-style code templates with a more powerful system should have loads of promise.

ImprobableTruth 6y ago
>Editing proofs written with tactics is a nightmare How so? Writing proofs in Agda is a joy, but it completely fails to document what I spend most of my time looking at: The context and the subgoal. Tactics only documenting this when you're able to step through them isn't something I'd hold against them, they're intended for interactive provers after all.
- ivanbakel 6y ago
  Well, in part because they don't document the context and the goal. Code has a clear context (variables and functions in scope) and a clear goal (return type). Editing code vs tactics is easy because the impact that each edit has on the context, goal, and code is clear and localised. Add or remove a tactic, and the rest of the proof can be completely invalidated. The fact that you can look at a code snippet and tell what it does, but looking at a tactic snippet essentially tells you nothing, is exemplary of the difference. Just the fact that you need a more powerful editing tool (interactive provers) to edit tactic proofs at all is testament to how much more complicated they are.
  - ImprobableTruth 6y ago
    >Code has a clear context (variables and functions in scope) and a clear goal (return type). At the top level, sure, but if you have a more complex proof term this breaks completely down. You'd have to evaluate potentially arbitrary expressions to determine the types and furthermore there is nothing to indicate the 'human' rather than mechanical structure of the proof since metavariables are just completely gone. It's just not my experience that I could look at a complex proof term (where I don't already know the underlying proof) and figure it out without using an interactive prover. >Add or remove a tactic, and the rest of the proof can be completely invalidated Just like if you randomly removed a part of a proof in term form it wouldn't typecheck anymore? 'stupid' tactics are just as localized as inserting the corresponding term with metavariables . If you're talking about how automation tactics are heavily context dependent, this is more of a fundamental quality of automation rather than tactics. Automation done via reflection suffers from the same issue.
avindroth 6y ago
In what ways is this way of programming different from Idris?
- cies 6y ago
  I also found this workflow is very similar to what I saw from Idris. I've come to know the practice as the "typed hole"[1] work flow. Idris is a different beast though, it has dependent types built in, where they come as an addon for Haskell. [1]: https://wiki.haskell.org/GHC/Typed_holes https://wiki.haskell.org/GHC/Typed_holes https://news.ycombinator.com/item?id=20435866 https://news.ycombinator.com/item?id=20435866
  - avindroth 6y ago
    I know of Hazel[1] as well. Is there a more free-form version of typed holes? The implementations here seem very cumbersome. Perhaps a version of this that has more focus on the duality of code as both runnable, complete code, and intermediate form between thought and code. [1]: https://hazel.org/ https://hazel.org/

ImprobableTruth 6y ago

>Editing proofs written with tactics is a nightmare How so? Writing proofs in Agda is a joy, but it completely fails to document what I spend most of my time looking at: The context and the subgoal. Tactics only documenting this when you're able to step through them isn't something I'd hold against them, they're intended for interactive provers after all.

ivanbakel 6y ago
Well, in part because they don't document the context and the goal. Code has a clear context (variables and functions in scope) and a clear goal (return type). Editing code vs tactics is easy because the impact that each edit has on the context, goal, and code is clear and localised. Add or remove a tactic, and the rest of the proof can be completely invalidated. The fact that you can look at a code snippet and tell what it does, but looking at a tactic snippet essentially tells you nothing, is exemplary of the difference. Just the fact that you need a more powerful editing tool (interactive provers) to edit tactic proofs at all is testament to how much more complicated they are.
- ImprobableTruth 6y ago
  >Code has a clear context (variables and functions in scope) and a clear goal (return type). At the top level, sure, but if you have a more complex proof term this breaks completely down. You'd have to evaluate potentially arbitrary expressions to determine the types and furthermore there is nothing to indicate the 'human' rather than mechanical structure of the proof since metavariables are just completely gone. It's just not my experience that I could look at a complex proof term (where I don't already know the underlying proof) and figure it out without using an interactive prover. >Add or remove a tactic, and the rest of the proof can be completely invalidated Just like if you randomly removed a part of a proof in term form it wouldn't typecheck anymore? 'stupid' tactics are just as localized as inserting the corresponding term with metavariables . If you're talking about how automation tactics are heavily context dependent, this is more of a fundamental quality of automation rather than tactics. Automation done via reflection suffers from the same issue.

avindroth 6y ago

In what ways is this way of programming different from Idris?

cies 6y ago
I also found this workflow is very similar to what I saw from Idris. I've come to know the practice as the "typed hole"[1] work flow. Idris is a different beast though, it has dependent types built in, where they come as an addon for Haskell. [1]: https://wiki.haskell.org/GHC/Typed_holes https://wiki.haskell.org/GHC/Typed_holes https://news.ycombinator.com/item?id=20435866 https://news.ycombinator.com/item?id=20435866
- avindroth 6y ago
  I know of Hazel[1] as well. Is there a more free-form version of typed holes? The implementations here seem very cumbersome. Perhaps a version of this that has more focus on the duality of code as both runnable, complete code, and intermediate form between thought and code. [1]: https://hazel.org/ https://hazel.org/