6 ms·

this looks really cool! I think it's weird that the author dings matlab and mathematica for being unable to do counterfactual reasoning. matlab and mathematica

by munin 11y ago

this looks really cool! I think it's weird that the author dings matlab and mathematica for being unable to do counterfactual reasoning. matlab and mathematica are computational tools, they don't do "reasoning" the way that say coq or other proof assistants do. and proof assistants can do counterfactual reasoning, so what's the deal? beyond that it would take a lot of work to encode these graphical diagrams into coq I guess...

conceit 11y ago
Matlab has a package for symbolic computation. It sounds to me like the author would want some of that, although I didn't quite follow through the whole argument.
seanmcdirmid 11y ago
I think he is arguing that they don't aid in counterfactual reasoning. They provide no facilities to help you yourself discover contradictions. This isn't about automating proofs, just helping you think through the problem.
- seanmcdirmid 11y ago
  Bah, I totally wrote this wrong. What I really meant to say was that it is not an automated system for doing a proof. It is a tool that helps you do reasoning and thinking. Augmenting human intelligence rather than replacing it.
  - munin 11y ago
    I think the proponents of proof assistants would say that the proof assistant is also there to help you do reasoning and thinking.
    - seanmcdirmid 11y ago
      I think they would! But a proof assistant aides you by checking your abstract thinking; you are still responsible for doing all the thinking yourself. This kind of tool aides in reasoning via a concrete example that can be tweaked in real time to see different sides of the problem.
      - catnaroek 11y ago
        > But a proof assistant aides you by checking your abstract thinking; you are still responsible for doing all the thinking yourself. This isn't really true. Nowadays, Coq can automate much of the process of coming up with a full proof - which is exactly what requires “abstract thinking”. (Of course, you still need to identify “strategic lemmas”, but even these lemmas can often be proven mostly automatically.) The downside is that machine-generated proofs are often gibberish from the point of view of human intelligibility, but that's okay if you're only interested in the truth of what is being proven. > This kind of tool aides in reasoning via a concrete example Actually, going from a concrete example to a more general abstract concept requires you to do the thinking yourself. At least if you want the result of the generalization process to be valid.
        seanmcdirmid 11y ago
        Surely Coq can fill in the wholes, but it is completely abstract; it doesn't use concrete examples to do this, and anyways, you really have to understand what it is doing. The point of this kind of work is that it augments your thinking by allowing you to visualize and manipulate your concrete example. Before, you'd just have pen and paper for that, with no assistance from the computer at all. The whole formal kick really comes after you have enough intuition about the problem, this comes before that and aides in the intuition accumulation process.
        catnaroek 11y ago
        Why do I need an intuition when I can just manipulate formulas?
        seanmcdirmid 11y ago
        Hey, isn't that it? Some people can just spend all their time in abstracting thinking land, manipulating formulas without concrete examples providing any context, because they have some amazing super power that many of us (maybe most?) don't have. Others need context. We need to see concrete examples of the problem, play around with them, explore them, until our brains can "get" a generalization. And in the end, maybe we all benefit from concrete context? When you are manipulating formulas, do you impose a concrete example in your head to guide that manipulation? Wouldn't it be great to get that out onto the computer somehow?

by munin 11y ago

conceit 11y ago

Matlab has a package for symbolic computation. It sounds to me like the author would want some of that, although I didn't quite follow through the whole argument.

seanmcdirmid 11y ago

I think he is arguing that they don't aid in counterfactual reasoning. They provide no facilities to help you yourself discover contradictions. This isn't about automating proofs, just helping you think through the problem.

seanmcdirmid 11y ago
Bah, I totally wrote this wrong. What I really meant to say was that it is not an automated system for doing a proof. It is a tool that helps you do reasoning and thinking. Augmenting human intelligence rather than replacing it.
- munin 11y ago
  I think the proponents of proof assistants would say that the proof assistant is also there to help you do reasoning and thinking.
  - seanmcdirmid 11y ago
    I think they would! But a proof assistant aides you by checking your abstract thinking; you are still responsible for doing all the thinking yourself. This kind of tool aides in reasoning via a concrete example that can be tweaked in real time to see different sides of the problem.
    - catnaroek 11y ago
      > But a proof assistant aides you by checking your abstract thinking; you are still responsible for doing all the thinking yourself. This isn't really true. Nowadays, Coq can automate much of the process of coming up with a full proof - which is exactly what requires “abstract thinking”. (Of course, you still need to identify “strategic lemmas”, but even these lemmas can often be proven mostly automatically.) The downside is that machine-generated proofs are often gibberish from the point of view of human intelligibility, but that's okay if you're only interested in the truth of what is being proven. > This kind of tool aides in reasoning via a concrete example Actually, going from a concrete example to a more general abstract concept requires you to do the thinking yourself. At least if you want the result of the generalization process to be valid.
      - seanmcdirmid 11y ago
        Surely Coq can fill in the wholes, but it is completely abstract; it doesn't use concrete examples to do this, and anyways, you really have to understand what it is doing. The point of this kind of work is that it augments your thinking by allowing you to visualize and manipulate your concrete example. Before, you'd just have pen and paper for that, with no assistance from the computer at all. The whole formal kick really comes after you have enough intuition about the problem, this comes before that and aides in the intuition accumulation process.
        catnaroek 11y ago
        Why do I need an intuition when I can just manipulate formulas?
        seanmcdirmid 11y ago
        Hey, isn't that it? Some people can just spend all their time in abstracting thinking land, manipulating formulas without concrete examples providing any context, because they have some amazing super power that many of us (maybe most?) don't have. Others need context. We need to see concrete examples of the problem, play around with them, explore them, until our brains can "get" a generalization. And in the end, maybe we all benefit from concrete context? When you are manipulating formulas, do you impose a concrete example in your head to guide that manipulation? Wouldn't it be great to get that out onto the computer somehow?