3 ms·

> 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 firs

> 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! Yep, there's no general algorithm for coming up with proofs. Practice, experience and good heuristics help, though. And if they don't, then you redesign the formal system until they do. > 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? Same as above. Just replace “proofs” with “programs”, and “formal system” with “programming language”. > Why use a list to store those elements? The desired invariants (see below) and complexity bounds for your code will tell you what data structures might be more convenient than others. > 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. I can't speak for others, but I really don't think that way. When I'm designing an algorithm, or when I'm trying to understand someone else's design, what matters to me first and foremost is its invariants - what the program preserves, even though the process' state is changing. Only if I can't see what the invariants are, then I might use some examples to generate plausible candidates, but the job isn't done until I have found and confirmed the invariants themselves. In other words, I don't conflate “works for these few examples” with “works in general”.

seanmcdirmid 11y ago
> Practice, experience and good heuristics help, though. And if they don't, then you redesign the formal system until they do. I'm not sure anyone really understands the cognitive processes behind doing math. But maybe? > The desired invariants (see below) and complexity bounds for your code will tell you what data structures might be more convenient than others. I rarely write code where I even need to think about complexity bounds! I'd be surprised if that was a dominating concern for even a significant fraction of programmers (systems HPC programmers, for sure, but...UI programmers?). > Only if I can't see what the invariants are, then I might use some examples to generate plausible candidates, but the job isn't done until I have found and confirmed the invariants themselves. In other words, I don't conflate “works for these few examples” with “works in general”. We don't. But you need to start somewhere. Don't underestimate the value of a few good examples in the problem solving process.
- catnaroek 11y ago
  > I'm not sure anyone really understands the cognitive processes behind doing math. As long as we all play by the rules of the symbolic game, I don't really need to understand what's going on inside anyone else's (or even my own) head. > I rarely write code where I even need to think about complexity bounds! I'd be surprised if that was a dominating concern for even a significant fraction of programmers (systems HPC programmers, for sure, but...UI programmers?). Invariants still remain, e.g., “the textboxes Red, Green, Blue, Hue, Saturation and Brightness must contain each a number between 0 and 255 inclusive; additionally, these numbers must satisfy the following equations (...)”. > We don't. But you need to start somewhere. Don't underestimate the value of a few good examples in the problem solving process. Oh, sure, examples can be a useful tool for finding the general rule, as I mentioned in my previous comment. But they don't replace the general rule.
seanmcdirmid 11y ago
Just to point out, I enjoyed our conversation. This is a debate that I think needs to happen.

seanmcdirmid 11y ago

> Practice, experience and good heuristics help, though. And if they don't, then you redesign the formal system until they do. I'm not sure anyone really understands the cognitive processes behind doing math. But maybe? > The desired invariants (see below) and complexity bounds for your code will tell you what data structures might be more convenient than others. I rarely write code where I even need to think about complexity bounds! I'd be surprised if that was a dominating concern for even a significant fraction of programmers (systems HPC programmers, for sure, but...UI programmers?). > Only if I can't see what the invariants are, then I might use some examples to generate plausible candidates, but the job isn't done until I have found and confirmed the invariants themselves. In other words, I don't conflate “works for these few examples” with “works in general”. We don't. But you need to start somewhere. Don't underestimate the value of a few good examples in the problem solving process.

catnaroek 11y ago
> I'm not sure anyone really understands the cognitive processes behind doing math. As long as we all play by the rules of the symbolic game, I don't really need to understand what's going on inside anyone else's (or even my own) head. > I rarely write code where I even need to think about complexity bounds! I'd be surprised if that was a dominating concern for even a significant fraction of programmers (systems HPC programmers, for sure, but...UI programmers?). Invariants still remain, e.g., “the textboxes Red, Green, Blue, Hue, Saturation and Brightness must contain each a number between 0 and 255 inclusive; additionally, these numbers must satisfy the following equations (...)”. > We don't. But you need to start somewhere. Don't underestimate the value of a few good examples in the problem solving process. Oh, sure, examples can be a useful tool for finding the general rule, as I mentioned in my previous comment. But they don't replace the general rule.

seanmcdirmid 11y ago

Just to point out, I enjoyed our conversation. This is a debate that I think needs to happen.