Awesome! I was just talking about this with a friend the other day. My formal education is in mathematics, but I've been writing software since high school.I wish Dan made his argument in a less pointed way, though.The underlying question is this: what does education look like on the web? Can every subject be taught there?In design, a skeuomorph is a derivative object that retains some feature of the original object which is no longer necessary. For example, iCal in OS X Lion looks like a physical calendar, even though there's no reason for a digital calendar to look (or behave) like a physical calendar. The same goes for the address book.This is what I see happening in online education. I don't think it's a case of "lol, Silicon Valley only trusts computers," but rather starting off by doing the most literal thing.Textbooks? Let's publish some PDFs online. Lectures? Let's publish videos online. Homework and tests? Let's make a website that works like a multiple-choice or fill-in-the-blank test.These are skeumorphs. There's no reason for the online equivalent of a textbook to be a PDF, it's just the most obvious thing.For me it's 1000x more interesting to ask "On the web, what's the best way to do what a lecture does offline?" than to say "Khan Academy videos are the wrong way of doing it."I think sites like Codecademy point the way when it comes to programming. The textbook is the IDE.What does that look like for math? It's much harder because, like Dan says, computers aren't the natural medium for mathematicians, so there will always be a translation step from math-ese to computer-ese.Once you're past basic math and are working out of a higher-level textbook, the exercises becomes very awkward to express on a computer in a way a computer can understand.And then grading -- oh boy!Take this, for example. Here is the first exercise from my first-year college calculus textbook (Michael Spivak's Calculus).`````` Prove: If ax = a for some number a != 0, then x = 1 `````` If you see that and think "That's easy enough to express in a way a computer understands, and there are proof verification systems" you're missing the point. No mathematician does his work that way. It would be like asking someone to learn programming by reading through a book and instead of writing`````` for(i = 0;i < n;i++) { printf("%d\n", i); } `````` you force students to write it down by hand in plain English instead of C. If you're an engineer, think of all the ink spent on whether whiteboard interviews are good or not. Asking mathematicians to do their work on a computer will get the same kind of response.(Empathy, brother!)The above was just my stream of consciousness, but I've been thinking about this for a bit now. Love this topic!*: Yes, I've seen his videos. They're fantastic and do a great job illustrating his educational philosophy.

 There are areas of mathematics for which proof assistants do a much better job; here is an interesting presentation using the theorem prover Coq as a virtual TA for discrete math: http://www.cis.upenn.edu/~bcpierce/papers/LambdaTA-ITP.pdfI want to take objection to the presentation of your example. It should be contextualized with the first chapter of Spivak's textbook, where he talks about algebraic properties of addition and multiplication for "numbers" (which aren't particularly well defined, but ostensibly since this is a Calculus textbook they are actually real numbers.) You can do these proofs fairly straightforwardly with rewrite rules, and proof assistants actually have rather good support for this. (The real difficulty shows up when you get to more complicated theorems, when we'd like to sweep rigor a little bit under the rug.) Look at the end of this book chapter for an exercise which asks the user to teach a proof assistant how to automatically show many simple properties of groups http://adam.chlipala.net/cpdt/html/LogicProg.html
 Thanks for the reply!I'll read that presentation when I get back. First impression: the author needs to learn about luminance as it applies to readability! Blue text on black background == headache.When you say "do a better job" what do you mean? I'd love to see papers about it.And yes, in that chapter you learn the field axioms and it's fairly straightforward for a computer to verify the statement given you present it to the computer in the correct way.That's my point, and I think Dan's point, too. Mathematicians don't do math that way.Like I said: "If you see that and think "That's easy enough to express in a way a computer understands, and there are proof verification systems" you're missing the point."As for http://adam.chlipala.net/cpdt/html/LogicProg.html, it looks relatively foreign to me. I'm going to read through it and figure it out, but would it helpful for a first-year college student who went from AP Calculus the previous year to Spivak's Calculus the next to be spending their time on logic programming?They've probably never even heard the word "lemma."++ It assumes you're at least a little proficient with the language of mathematics.Pointing to things like Coq as a solution is like telling an average computer user, "Why use Dropbox when you can just use rsync and some shell scripts?"It might be the basis for something better designed, but it's only part of a larger, hitherto undiscovered, solution.++: I'm describing my experience. Spivak was the first time I was introduced to the proof-as-exercise paradigm that's the cornerstone of every higher-math textbook.
 Proof assistants have close ties to logic and type theory, so it's not much surprise that they're quite good for doing this small, subarea of mathematics. (Indeed, I think in the not too distant future we will be teaching logic using something like an interactive theorem prover. It makes a bit of the formalism quite clearer.) There has been some push, especially in Europe, for using these programs to prove other mathematics; it is certainly possible, although few would say it is pleasant or resembles how ordinary mathematicians work. But I think that, for specific areas of mathematics, these tools are useful today. Especially when trying to teach students how to think formally; you'll find that formal corresponds closely to how the computer thinks about things (and the whole problem is that mathematicians are not very formal at all.)CPDT is not a good first text; Software Foundations http://www.cis.upenn.edu/~bcpierce/sf/ does better for people with less math experience.
 I just went through the presentation. It's an interesting experiment, but seems completely unsuitable for teaching the example I gave from Spivak to a first-year college student with no prior exposure to CS or formal mathematics.It might be useful to someone who has a extensive background in functional programming, but it's in a completely different universe than the one most mathematicians live in.
 I agree that at this point, it's completely unsuitable for the staples of college mathematics (e.g. calculus, differential equations), although it was not clear non-mathematicians were being subject to any sort of rigor anyway.That said, these tools have been used to teach Freshmen CS majors, and to reasonably good effect.

Search: