7 ms·

I hate to be a downer, but I just don't trust automatic code generation. Proof automation is nice because proofs are ultimately irrelevant. It doesn't matter w

I hate to be a downer, but I just don't trust automatic code generation. Proof automation is nice because proofs are ultimately irrelevant. It doesn't matter what the proof is, only that there is one. With code, it's another matter. If I have to depend on heuristics for it to choose the right option that means that I'll actually have to read and verify whether it chose the correct one. At that point, I feel like I'm not really winning anything over just writing it myself. It's possible to write a complex specification to ensure the generated code would be correct, but current automation already struggles with generating proofs for hand written code, let alone generating code and verifying it. Also, it isn't clear to me whether tactics programs are supposed to be kept as code or just used by the LSP which the gif makes it seem like. To me the strongest benefits of tactics are that they can be used to document what the author was trying to do and that using an IDE they can be executed step-by-step. If it's just to be used by the LSP: What is the point of using tactics vs normal metaprogramming?

ivanbakel 6y ago
Note that these are tactics for metaprogramming - the tactics are themselves for programming, not for use in programs. The commands to the LSP tell it how to generate the code, and the code sticks around for editing afterwards. >If it's just to be used by the LSP: What is the point of using tactics vs normal metaprogramming? What is "normal" metaprogramming? The particular benefit of using tactics would be that they're designed for small steps of in-flight editing, rather than generating something all at once; and that their vocabulary is pretty well established.
- ImprobableTruth 6y ago
  >Note that these are tactics for metaprogramming - the tactics are themselves for programming, not for use in programs. I don't understand what this is supposed to mean. How are e.g. coq tactics not the exact same? >The commands to the LSP tell it how to generate the code, and the code sticks around for editing afterwards. Not having the metaprogram which generated the code around just strikes me more as an anti-feature. >What is "normal" metaprogramming? Arbitrary, "non-sequential" code transformations. >The particular benefit of using tactics would be that they're designed for small steps of in-flight editing, rather than generating something all at once Well, for me tactics definitely invokes more serious proof automation than just what you could also do using Agda's emacs commands. This is also the impression I get from the article, the image presented uses some form of auto tactic to generate an entire term in one go. Certainly not what I'd call "small steps of in-flight editing".
  - remexre 6y ago
    > I don't understand what this is supposed to mean. How are e.g. coq tactics not the exact same? Well, I've never gotten `induction' to generate anything close to a readable program -- hopefully this is better?
    - ImprobableTruth 6y ago
      I'm not sure what you mean? The induction tactic uses the induction principle (dependent eliminator) of the corresponding type. If you unfold the dependent eliminator, it boils down to a combination of fix and match. I don't see how you could get a term simpler than that, unless you mean something else by readable?
      - remexre 6y ago
        IIRC, the match it generates often ends up being a dependent match using the convoy pattern once nontrivial functions start being written, which quickly gets really really hard to read. Maybe this is partly the fault of Coq's matching requiring the convoy pattern (unlike Agda's or Idris's), but I find it extremely difficult to read these terms, versus hand-written ones.
  - ivanbakel 6y ago
    >I don't understand what this is supposed to mean. How are e.g. coq tactics not the exact same? Coq tactics are code - you write terms using tactics, and you edit the term by editing the tactics. Save and load the file, and only the tactics stick around. In this version, tactics write code - you use tactics to generate a term (Haskell code), and then you can edit the term itself. Save and load the file, and all you get is the Haskell code: the tactics only existed for codegen. >Not having the metaprogram which generated the code around just strikes me more as an anti-feature. Why? The trouble with metaprogramming is that you basically never want to have the power to simultaneously edit the program and the metaprogram. As you yourself pointed out, tactics would be terrible as an opaque metaprogram - they only work if you don't care about the particular term they generate. Tactic metaprogramming lets you write terms quickly - it fulfills a need that lots of Haskell programmers have, which is that certain type signatures have "obvious" inhabitants and actually expressing those inhabitants can itself feel like a lot of boilerplate. But since you need to edit the Haskell code itself, the metaprogram must disappear. You won't miss it, since you won't need to regenerate the program from the metaprogram. >the image presented uses some form of auto tactic to generate an entire term in one go Because it's built out of several tactic steps, which the article goes into the construction of. You could still (presumably) have built it piece by piece, by applying each tactic one at a time - and each step only modifies the term slightly, leaving a hole for later steps.
- vii 6y ago
  For the recursive functor application example on a tree, normal meta-programming would be a macro taking the type as an argument, and then generating the resulting case by case application code, at compile time. This would be much clearer and could automatically keep working if more cases were added (adding new node types is common when adding language features to abstract syntax trees). This is a very awesome demo but my experience with other templating systems in IDEs (like autogenerated toString and other methods in Java) is that making boilerplate easy to write doesn't help make it easier to read or modify.
whateveracct 6y ago
> Also, it isn't clear to me whether tactics programs are supposed to be kept as code or just used by the LSP which the gif makes it seem like. I'm pretty sure you use it as a starting point and then go from there. Saves a good amount of mechanical work.
lalaithion 6y ago
I agree; the most exciting use case for a system like this would be that it would functionally (no pun intended) replace the idea of "tab-completion" for typed functional programming languages.
zokier 6y ago
> I hate to be a downer, but I just don't trust automatic code generation. Isn't all programming in high level languages really just automatic code generation? https://en.wikipedia.org/wiki/Autocode https://en.wikipedia.org/wiki/Autocode

ivanbakel 6y ago

Note that these are tactics for metaprogramming - the tactics are themselves for programming, not for use in programs. The commands to the LSP tell it how to generate the code, and the code sticks around for editing afterwards. >If it's just to be used by the LSP: What is the point of using tactics vs normal metaprogramming? What is "normal" metaprogramming? The particular benefit of using tactics would be that they're designed for small steps of in-flight editing, rather than generating something all at once; and that their vocabulary is pretty well established.

ImprobableTruth 6y ago
>Note that these are tactics for metaprogramming - the tactics are themselves for programming, not for use in programs. I don't understand what this is supposed to mean. How are e.g. coq tactics not the exact same? >The commands to the LSP tell it how to generate the code, and the code sticks around for editing afterwards. Not having the metaprogram which generated the code around just strikes me more as an anti-feature. >What is "normal" metaprogramming? Arbitrary, "non-sequential" code transformations. >The particular benefit of using tactics would be that they're designed for small steps of in-flight editing, rather than generating something all at once Well, for me tactics definitely invokes more serious proof automation than just what you could also do using Agda's emacs commands. This is also the impression I get from the article, the image presented uses some form of auto tactic to generate an entire term in one go. Certainly not what I'd call "small steps of in-flight editing".
- remexre 6y ago
  > I don't understand what this is supposed to mean. How are e.g. coq tactics not the exact same? Well, I've never gotten `induction' to generate anything close to a readable program -- hopefully this is better?
  - ImprobableTruth 6y ago
    I'm not sure what you mean? The induction tactic uses the induction principle (dependent eliminator) of the corresponding type. If you unfold the dependent eliminator, it boils down to a combination of fix and match. I don't see how you could get a term simpler than that, unless you mean something else by readable?
    - remexre 6y ago
      IIRC, the match it generates often ends up being a dependent match using the convoy pattern once nontrivial functions start being written, which quickly gets really really hard to read. Maybe this is partly the fault of Coq's matching requiring the convoy pattern (unlike Agda's or Idris's), but I find it extremely difficult to read these terms, versus hand-written ones.
- ivanbakel 6y ago
  >I don't understand what this is supposed to mean. How are e.g. coq tactics not the exact same? Coq tactics are code - you write terms using tactics, and you edit the term by editing the tactics. Save and load the file, and only the tactics stick around. In this version, tactics write code - you use tactics to generate a term (Haskell code), and then you can edit the term itself. Save and load the file, and all you get is the Haskell code: the tactics only existed for codegen. >Not having the metaprogram which generated the code around just strikes me more as an anti-feature. Why? The trouble with metaprogramming is that you basically never want to have the power to simultaneously edit the program and the metaprogram. As you yourself pointed out, tactics would be terrible as an opaque metaprogram - they only work if you don't care about the particular term they generate. Tactic metaprogramming lets you write terms quickly - it fulfills a need that lots of Haskell programmers have, which is that certain type signatures have "obvious" inhabitants and actually expressing those inhabitants can itself feel like a lot of boilerplate. But since you need to edit the Haskell code itself, the metaprogram must disappear. You won't miss it, since you won't need to regenerate the program from the metaprogram. >the image presented uses some form of auto tactic to generate an entire term in one go Because it's built out of several tactic steps, which the article goes into the construction of. You could still (presumably) have built it piece by piece, by applying each tactic one at a time - and each step only modifies the term slightly, leaving a hole for later steps.
vii 6y ago
For the recursive functor application example on a tree, normal meta-programming would be a macro taking the type as an argument, and then generating the resulting case by case application code, at compile time. This would be much clearer and could automatically keep working if more cases were added (adding new node types is common when adding language features to abstract syntax trees). This is a very awesome demo but my experience with other templating systems in IDEs (like autogenerated toString and other methods in Java) is that making boilerplate easy to write doesn't help make it easier to read or modify.

whateveracct 6y ago

> Also, it isn't clear to me whether tactics programs are supposed to be kept as code or just used by the LSP which the gif makes it seem like. I'm pretty sure you use it as a starting point and then go from there. Saves a good amount of mechanical work.

lalaithion 6y ago

I agree; the most exciting use case for a system like this would be that it would functionally (no pun intended) replace the idea of "tab-completion" for typed functional programming languages.

zokier 6y ago

> I hate to be a downer, but I just don't trust automatic code generation. Isn't all programming in high level languages really just automatic code generation? https://en.wikipedia.org/wiki/Autocode https://en.wikipedia.org/wiki/Autocode