5 ms·

I think the proponents of proof assistants would say that the proof assistant is also there to help you do reasoning and thinking.

by munin 11y ago

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?
        catnaroek 11y ago
        I see two concerns being conflated here: (0) how to motivate the study of a formal system, and (1) how to actually study the formal system. To motivate the study of a formal system, that is, to convince someone that the system is useful, obviosuly you need examples and applications. To a non-mathematician like me, that motivation must come from outside mathematics, e.g., how to design and write reliable programs that are easy to understand and maintain. But, once you have decided that a formal system is useful, you really need to understand it in its own terms. You seem to view formulas as “too abstract”, and in need of “explanation” (not just motivation) in terms of something “more concrete”. I don't see why. By itself, a formula is nothing but a well-formed syntax tree, that is, a data structure just like lists or arrays (though usually with more complex internal invariants). Do you think lists and arrays are in need of “explanation”? The rules for manipulating formulas are themselves also fairly mechanical and concrete, just like the rules for manipulating lists and arrays. Or am I missing something?
        seanmcdirmid 11y ago
        This isn't about motivation. Its not even about study, rather how do you go about doing formal reasoning at all? Prove X has property P, what is even the first step? How do we get to the second step, and so on? Doing a proof is not a mechanical process, there isn't an algorithm for deciding what to do next to reach your goal! Programming is a great example of this. Those lists and arrays don't appear out of nowhere. Someone has to write the code, how do they write the code? Why use a list to store those elements? Programs are generalized to operate on a wide variety of inputs to create a wide variety of outputs, but when you are writing code, you are thinking about just a few examples of those, you imagine them in your head and they guide the code you write. But perhaps the computer could help there as well.

I think the proponents of proof assistants would say that the proof assistant is also there to help you do reasoning and thinking.

by 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?
      - catnaroek 11y ago
        I see two concerns being conflated here: (0) how to motivate the study of a formal system, and (1) how to actually study the formal system. To motivate the study of a formal system, that is, to convince someone that the system is useful, obviosuly you need examples and applications. To a non-mathematician like me, that motivation must come from outside mathematics, e.g., how to design and write reliable programs that are easy to understand and maintain. But, once you have decided that a formal system is useful, you really need to understand it in its own terms. You seem to view formulas as “too abstract”, and in need of “explanation” (not just motivation) in terms of something “more concrete”. I don't see why. By itself, a formula is nothing but a well-formed syntax tree, that is, a data structure just like lists or arrays (though usually with more complex internal invariants). Do you think lists and arrays are in need of “explanation”? The rules for manipulating formulas are themselves also fairly mechanical and concrete, just like the rules for manipulating lists and arrays. Or am I missing something?
        seanmcdirmid 11y ago
        This isn't about motivation. Its not even about study, rather how do you go about doing formal reasoning at all? Prove X has property P, what is even the first step? How do we get to the second step, and so on? Doing a proof is not a mechanical process, there isn't an algorithm for deciding what to do next to reach your goal! Programming is a great example of this. Those lists and arrays don't appear out of nowhere. Someone has to write the code, how do they write the code? Why use a list to store those elements? Programs are generalized to operate on a wide variety of inputs to create a wide variety of outputs, but when you are writing code, you are thinking about just a few examples of those, you imagine them in your head and they guide the code you write. But perhaps the computer could help there as well.