5 ms·

> it could be proved with just a single "by arith". Tactics are probably a usability improvement for mathematicians who are used to proving everything by hand.

> it could be proved with just a single "by arith". Tactics are probably a usability improvement for mathematicians who are used to proving everything by hand. But for programmers used to type inference, they're a step backwards. Mathematicians typically prove much deeper results, but they do so at a much slower rate than programmers write programs.

Ericson2314 10y ago
Huh tactics are pretty great. Say exactly what you want and the computer programs itself! It's unfair to just compare development time between tactic-generated programs in a dependent language with manually written programs in a non-depenendent language. The end result in the dependent language is much more valuable.
- catnaroek 10y ago
  I'm not comparing dependent types vs. no dependent types. I'm comparing higher-order dependent types (Agda, Idris, Coq, etc.) vs. first-order dependent types: https://news.ycombinator.com/item?id=12350147 https://news.ycombinator.com/item?id=12350147 Seriously, Coq-style proof scripts are utterly unredable when they grow past a certain size. The only way to understand them is to replay them, so that you can see the intermediate hypotheses and goals.
  - harveywi 10y ago
    > The only way to understand them is to replay them Reminds me of the same kind of problem that arises in trying to understand the runtime behavior of nontrivial programs involving side-effects, mutable state, multithreading, etc. Sometimes the debugger is the only practical way to figure out what the program is doing. Add concurrency into the mix, and things can get tricky very quickly. Dependently-typed programming and machine-assisted proof is still an emerging thing, and there is probably lots of room for exploring ergonomic improvements. It will be interesting to see where this goes.
    - catnaroek 10y ago
      Your analogy between debugging effectful programs and replaying proof scripts is frighteningly accurate.
  - mietek 10y ago
    I agree. Note that the Coq-style tactics-based approach is not the only possibility. In Agda, you are expected to write proofs in a functional style, similar to Haskell programs. There is a small amount of integrated automation, which helps you fill in holes in your proofs — however, the results are explicit proof terms, inserted at the right place in your program. Systems which behave in this fashion have the de Bruijn criterion, as described in Geuvers (2009) “Proof assistants: History, ideas, and future”. https://www.dropbox.com/s/4mwtxojg7yqb365/Geuvers2009.pdf https://www.dropbox.com/s/4mwtxojg7yqb365/Geuvers2009.pdf
    - catnaroek 10y ago
      Thanks for the links (this one and the one from your other reply), I'm checking them.
    - deleted 10y ago
      [deleted]
  - matej_kosik 10y ago
    I had/have a similar feeling. I have thought about it some time ago and came up with the following proposal: http://matej-kosik.github.io/www/doc/coq/coq-trunk-proof-tree/index.html http://matej-kosik.github.io/www/doc/coq/coq-trunk-proof-tre...
imh 10y ago
That's mostly true, but the speed programmers write programs depends how bulletproof they have to be. There have been times that if you include the debugging and maintainability difficulty, proving things to my compiler would be a step forward for me. There's probably a sweet spot.
- catnaroek 10y ago
  > That's mostly true, but the speed programmers write programs depends how bulletproof they have to be. Of course, but, in any case, writing programs at the same rate mathematicians prove theorems simply isn't viable.

Ericson2314 10y ago

Huh tactics are pretty great. Say exactly what you want and the computer programs itself! It's unfair to just compare development time between tactic-generated programs in a dependent language with manually written programs in a non-depenendent language. The end result in the dependent language is much more valuable.

catnaroek 10y ago
I'm not comparing dependent types vs. no dependent types. I'm comparing higher-order dependent types (Agda, Idris, Coq, etc.) vs. first-order dependent types: https://news.ycombinator.com/item?id=12350147 https://news.ycombinator.com/item?id=12350147 Seriously, Coq-style proof scripts are utterly unredable when they grow past a certain size. The only way to understand them is to replay them, so that you can see the intermediate hypotheses and goals.
- harveywi 10y ago
  > The only way to understand them is to replay them Reminds me of the same kind of problem that arises in trying to understand the runtime behavior of nontrivial programs involving side-effects, mutable state, multithreading, etc. Sometimes the debugger is the only practical way to figure out what the program is doing. Add concurrency into the mix, and things can get tricky very quickly. Dependently-typed programming and machine-assisted proof is still an emerging thing, and there is probably lots of room for exploring ergonomic improvements. It will be interesting to see where this goes.
  - catnaroek 10y ago
    Your analogy between debugging effectful programs and replaying proof scripts is frighteningly accurate.
- mietek 10y ago
  I agree. Note that the Coq-style tactics-based approach is not the only possibility. In Agda, you are expected to write proofs in a functional style, similar to Haskell programs. There is a small amount of integrated automation, which helps you fill in holes in your proofs — however, the results are explicit proof terms, inserted at the right place in your program. Systems which behave in this fashion have the de Bruijn criterion, as described in Geuvers (2009) “Proof assistants: History, ideas, and future”. https://www.dropbox.com/s/4mwtxojg7yqb365/Geuvers2009.pdf https://www.dropbox.com/s/4mwtxojg7yqb365/Geuvers2009.pdf
  - catnaroek 10y ago
    Thanks for the links (this one and the one from your other reply), I'm checking them.
  - deleted 10y ago
    [deleted]
- matej_kosik 10y ago
  I had/have a similar feeling. I have thought about it some time ago and came up with the following proposal: http://matej-kosik.github.io/www/doc/coq/coq-trunk-proof-tree/index.html http://matej-kosik.github.io/www/doc/coq/coq-trunk-proof-tre...

imh 10y ago

That's mostly true, but the speed programmers write programs depends how bulletproof they have to be. There have been times that if you include the debugging and maintainability difficulty, proving things to my compiler would be a step forward for me. There's probably a sweet spot.

catnaroek 10y ago
> That's mostly true, but the speed programmers write programs depends how bulletproof they have to be. Of course, but, in any case, writing programs at the same rate mathematicians prove theorems simply isn't viable.