8 ms·

If you view it in terms of psychological development, understanding concrete imperative steps happens before children are capable of understanding abstract conc

If you view it in terms of psychological development, understanding concrete imperative steps happens before children are capable of understanding abstract concepts like mathematics. The works of Seymour Papert describe how these findings relate to education. That said, people who connect this to software in a professional context are doing a disservice since hopefully software professionals have progressed in their intellectual development beyond their teens and are capable of abstract mathematical thought.

pron 10y ago
Concrete imperative steps are extremely mathematical -- even elegantly so -- and most of software verification is predicated on this idea. Just like you can describe physics pretty precisely with simple math, you can do it with computation. The math of PFP is one particular approximation, chosen for its supposed utility as the basis for a language. It is more linguistic math than descriptive math. I also hope people adopt abstract mathematical thought when reasoning about their programs, but that has little to do with the kind of math they choose to model their programs' source code with.
- johncolanduoni 10y ago
  Sure, you can model imperative steps in a variety of ways using mathematics, but for 99% of mathematics there is a far more direct link to pure functions. In how many branches of mathematics do you see a function that is anything but a mapping between sets (or types, or objects in a category). In terms of using the same kind of processes and intuitions, pure functional programming is much closer to mathematics as done by humans than imperative programming. Even theoretical computer science looks this way outside of particular algorithms being studied. Not that this is some sort of indictment of imperative programming; it's a much better fit for a lot of different situations. But if you're trying to model something in abstract mathematics, pure or pure-ish function programming is likely to be a better solution. For example, look at the various proof assistants like Coq. Many of them are written in functional languages, and if you look at the code you can see why: the manipulation of formulas and proofs fits very well with an immutable, functional approach.
  - pron 10y ago
    > but for 99% of mathematics there is a far more direct link to pure functions. But state transitions are pure! Deterministic state machines are nothing more than mathematical functions from one algorithm state to the next, and nondeterministic ones are binary relations! (see this for an overview: http://research.microsoft.com/en-us/um/people/lamport/pubs/state-machine.pdf http://research.microsoft.com/en-us/um/people/lamport/pubs/s...) Those can then be mathematically manipulated, substituted and what-have-you elegantly and simply. This is how formal verification has been reasoning about programs since the seventies (early on the formalization was a bit more cumbersome, but the concept was as simple). > For example, look at the various proof assistants like Coq. For example, look at the specification language (and proof assistant) TLA+. It is far simpler than Coq, just as pure, and requires no more than highschool math. Coq and other PFP formalizations are built on the core idea of denotational semantics, an approximation which at times only complicates the very simple math of computation, requiring exotic math like category theory. > the manipulation of formulas and proofs fits very well with an immutable, functional approach. The manipulation of formulas and proofs fits very well with the imperative approach, only no category theory is required, and core concepts such as simulation/trace-inclusion arise naturally without need for complex embeddings. "PFP math" is what arises after you've decided to use denotational semantics. The most important thing is not to confuse language -- for which PFP has an elegant albeit arcane mathematical formalization -- with the very simple mathematical concepts underlying computation. PFP is an attempt to apply one specific mathematical formulation to programming languages (other similar, though perhaps less successful attempts are the various process calculi). But it is by no means the natural mathematics of computation. Conflating language with algorithms is a form of deconstructionism: an interesting philosophical concept, but by no means a simple one, and perhaps not the most appropriate one for a science. Short of that, we have the basic, simple core math, and on top of it languages, some espousing various mathematical formalizations, related to the core math in interesting ways, and some less mathematical. But the math of computation isn't created by the language!
    - johncolanduoni 10y ago
      > But state transitions are pure! Deterministic state machines are nothing more than (obviously, "pure") functions from one program state to the next, and nondeterministic ones are binary relations! Okay, yes, but 99% of mathematics isn't deterministic state machines. So again, pure functions can model a lot of things, but deterministic state machines are foreign to the way people think about mathematics in most instances. > For example, look at the pure specification language (and proof assistant) TLA+. It is far simpler than Coq, just as pure, and requires no more than highschool math. Okay, that's completely fine as an example. I just mentioned Coq because it's one of the better known ones. > Coq and other PFP formalizations are built on the core idea of denotational semantics, an approximation which at times only complicates the very simple math of computation, requiring exotic math like category theory. I'm not sure where CiC (or any of the other recent type theories, including HOTT) requires category theory (which is hardly exotic in 2016). People who are doing meta-mathematics on these systems are interested in categorical models and such, but implementing and using these systems requires no category theory. Categories are not fundamental objects in these theories; you have to build them just like you do in material set theories, although some parts of that process are easier (especially in HOTT). But that is the reverse of the link that you're claiming. > The manipulation of formulas and proofs fits very well with the imperative approach, only no category theory is required, and core concepts such as simulation/trace-inclusion arise naturally without need for complex embeddings. Again, no category theory is required (though I'm still not sure why this is a bad thing?) to develop a prover like Coq or TLA+. If you're bringing simulation and trace-inclusion into this, then you're just saying the stateful, imperative approach is well adapted to working with stateful, imperative systems. I agree, but how exactly does that equate to that approach having any benefit whatsoever for formalizing the rest of mathematics?
ayberkt 10y ago
That's a great point, thanks! I will look into Papert's work. Are there any specific papers/books you would recommend?
- technomancy 10y ago
  Well the classic here is his book Mindstorms where he talks about how to construct learning environments for children that take into account that bridge between concrete and abstract thought and turn it into an asset instead of a liability. If you want more on the topic that's not from the hands-on perspective of an educator, you might have to go further back to Piaget's papers, but unfortunately I haven't had the opportunity to dive into these much.

pron 10y ago

Concrete imperative steps are extremely mathematical -- even elegantly so -- and most of software verification is predicated on this idea. Just like you can describe physics pretty precisely with simple math, you can do it with computation. The math of PFP is one particular approximation, chosen for its supposed utility as the basis for a language. It is more linguistic math than descriptive math. I also hope people adopt abstract mathematical thought when reasoning about their programs, but that has little to do with the kind of math they choose to model their programs' source code with.

johncolanduoni 10y ago
Sure, you can model imperative steps in a variety of ways using mathematics, but for 99% of mathematics there is a far more direct link to pure functions. In how many branches of mathematics do you see a function that is anything but a mapping between sets (or types, or objects in a category). In terms of using the same kind of processes and intuitions, pure functional programming is much closer to mathematics as done by humans than imperative programming. Even theoretical computer science looks this way outside of particular algorithms being studied. Not that this is some sort of indictment of imperative programming; it's a much better fit for a lot of different situations. But if you're trying to model something in abstract mathematics, pure or pure-ish function programming is likely to be a better solution. For example, look at the various proof assistants like Coq. Many of them are written in functional languages, and if you look at the code you can see why: the manipulation of formulas and proofs fits very well with an immutable, functional approach.
- pron 10y ago
  > but for 99% of mathematics there is a far more direct link to pure functions. But state transitions are pure! Deterministic state machines are nothing more than mathematical functions from one algorithm state to the next, and nondeterministic ones are binary relations! (see this for an overview: http://research.microsoft.com/en-us/um/people/lamport/pubs/state-machine.pdf http://research.microsoft.com/en-us/um/people/lamport/pubs/s...) Those can then be mathematically manipulated, substituted and what-have-you elegantly and simply. This is how formal verification has been reasoning about programs since the seventies (early on the formalization was a bit more cumbersome, but the concept was as simple). > For example, look at the various proof assistants like Coq. For example, look at the specification language (and proof assistant) TLA+. It is far simpler than Coq, just as pure, and requires no more than highschool math. Coq and other PFP formalizations are built on the core idea of denotational semantics, an approximation which at times only complicates the very simple math of computation, requiring exotic math like category theory. > the manipulation of formulas and proofs fits very well with an immutable, functional approach. The manipulation of formulas and proofs fits very well with the imperative approach, only no category theory is required, and core concepts such as simulation/trace-inclusion arise naturally without need for complex embeddings. "PFP math" is what arises after you've decided to use denotational semantics. The most important thing is not to confuse language -- for which PFP has an elegant albeit arcane mathematical formalization -- with the very simple mathematical concepts underlying computation. PFP is an attempt to apply one specific mathematical formulation to programming languages (other similar, though perhaps less successful attempts are the various process calculi). But it is by no means the natural mathematics of computation. Conflating language with algorithms is a form of deconstructionism: an interesting philosophical concept, but by no means a simple one, and perhaps not the most appropriate one for a science. Short of that, we have the basic, simple core math, and on top of it languages, some espousing various mathematical formalizations, related to the core math in interesting ways, and some less mathematical. But the math of computation isn't created by the language!
  - johncolanduoni 10y ago
    > But state transitions are pure! Deterministic state machines are nothing more than (obviously, "pure") functions from one program state to the next, and nondeterministic ones are binary relations! Okay, yes, but 99% of mathematics isn't deterministic state machines. So again, pure functions can model a lot of things, but deterministic state machines are foreign to the way people think about mathematics in most instances. > For example, look at the pure specification language (and proof assistant) TLA+. It is far simpler than Coq, just as pure, and requires no more than highschool math. Okay, that's completely fine as an example. I just mentioned Coq because it's one of the better known ones. > Coq and other PFP formalizations are built on the core idea of denotational semantics, an approximation which at times only complicates the very simple math of computation, requiring exotic math like category theory. I'm not sure where CiC (or any of the other recent type theories, including HOTT) requires category theory (which is hardly exotic in 2016). People who are doing meta-mathematics on these systems are interested in categorical models and such, but implementing and using these systems requires no category theory. Categories are not fundamental objects in these theories; you have to build them just like you do in material set theories, although some parts of that process are easier (especially in HOTT). But that is the reverse of the link that you're claiming. > The manipulation of formulas and proofs fits very well with the imperative approach, only no category theory is required, and core concepts such as simulation/trace-inclusion arise naturally without need for complex embeddings. Again, no category theory is required (though I'm still not sure why this is a bad thing?) to develop a prover like Coq or TLA+. If you're bringing simulation and trace-inclusion into this, then you're just saying the stateful, imperative approach is well adapted to working with stateful, imperative systems. I agree, but how exactly does that equate to that approach having any benefit whatsoever for formalizing the rest of mathematics?

ayberkt 10y ago

That's a great point, thanks! I will look into Papert's work. Are there any specific papers/books you would recommend?

technomancy 10y ago
Well the classic here is his book Mindstorms where he talks about how to construct learning environments for children that take into account that bridge between concrete and abstract thought and turn it into an asset instead of a liability. If you want more on the topic that's not from the hands-on perspective of an educator, you might have to go further back to Piaget's papers, but unfortunately I haven't had the opportunity to dive into these much.