"Wadler created ML to help automate proofs".
Minor nitpick: actually, ML was designed by Robin Milner: http://en.wikipedia.org/wiki/ML_(programming_language)
1,476 karma · joined December 26, 2009
A hello world sample: http://hopl.murdoch.edu.au/showexample.prx?exp=59
See the C# specification section 9.2.3 (grammar ambiguities) for more details: http://www.ecma-international.org/publications/files/ECMA-ST...
LtU has a thread on Rust: http://lambda-the-ultimate.org/node/4009
The most interesting feature is the use of linear types to statically ensure sound usage of resources, including memory, in other words, no garbage collector.
Seibel: Speaking of practical work, in the middle of working on The Art of Computer Programming you took what turned into a ten-year break to write your typesetting system TeX. I understand you wrote the first version of TeX completely away from the computer.
Knuth: When I wrote TeX originally in 1977 and ’78, of course I didn’t have literate programming but I did have structured programming. I wrote it in a big notebook in longhand, in pencil. Six months later, after I had gone through the whole project, I started typing into the computer. And did the debugging in March of ’78 while I had started writing the program in October of ’77. The code for that is in the Stanford archives—it’s all in pencil—and of course I would come back and change a subroutine as I learned what it should be. This was a first-generation system, so lots of different architectures were possible and had to be discarded until I’d lived with it for a while and knew what was there. And it was a chicken-and-egg problem—you couldn’t typeset until you had fonts but then you couldn’t have fonts until you could typeset. But structured programming gave me the idea of invariants and knowing how to make black boxes that I could understand. So I had the confidence that the code would work when I finally would debug it. I felt that I would be saving a lot of time if I waited six months before testing anything. I had enough confidence that the code was approximately right.
Seibel: And the time savings would be because you wouldn’t spend time building scaffolding and stubs to test incomplete code?
Knuth: Right.
http://richarddawkins.net/articles/824-postmodernism-disrobe...
Fun fact: Doron is known for crediting his computer "Shalosh B. Ekhad" as a co-author.
Disciple is pure. This is argued in the first chapter of Ben Lippmeier's thesis: http://www.cse.unsw.edu.au/~benl/papers/thesis/lippmeier-imp...
Interesting discussion of why Dijkstra hated APL so much: http://www.mail-archive.com/chat@jsoftware.com/msg00137.html
More: http://www.janestreetcapital.com/minsky_weeks-jfp_18.pdf
blah blah blah dependency injection blah blah blah (This is a bit off-topic, but it came to mind, so what the hell.) You are correct in your observations that given most programming languages (even those such as Haskell), it is difficult to see exactly how Curry-Howard is useful. I recently stumbled across someone mentioning something called "dependency injection". I didn't know what it was, so I googled (I guess this is lowercase nowadays!) it and read Martin Fowler's article on it. It is a bit on the long side, and I kept waiting for the punch-line; you know, the point at which the author hits you with the insight which justifies the preceding verbosity and the hi-tech-sounding name ("dependency injection" — I can't help but think of "fuel injection", and gleaming motor engine showcases), but it seemed indefinitely postponed. And in the end, it turned out that "dependency injection" just means "abstraction" specifically by parametrization, by update and by what I think amounts to type abstraction plus update. (Apparently these are called — I kid you not — type 3 IoC, type 2 IoC and type 1 IoC...!) To me this all seemed rather obvious and it got me thinking about why it isn't obvious to the author or his readership. In Haskell, if I am given some type B which I need to produce somehow, and I realize that the B-values I need depend on some other values of type A, the first thing I do is write down "f :: A -> B". Then I write down "f a =", and then I start writing stuff after the equals sign until I have what I need. I do that because I know once I have the type that if there is an inhabitant of the type "A -> B" it can be expressed as "\a -> b" for some b, so the "f a =" part is always part of my solution and I will never have to change that unless I want to. So once I've written that down I feel one step closer to my solution. I know that for three reasons. First, because of my experience as a functional programmer. Second, because it is part of the universal property of exponentials ("factors uniquely"), that is, of function types. And third, because by the Curry-Howard correspondence with natural deduction, I can start any proof of A which depends on B by assuming A, that is, adding it as a hypothesis. So, why is it so obscure in Java? I think part of the reason is that in Java you have update, so there are complications and additional solutions. But part of the reason is also that it largely lacks structural typing, and that makes it hard to see that a class('s interface) is a product of exponentials. (With nominal typing, you tend to think of a class by its name, rather than its structure.) You could also blame the syntax of method signatures, which obscure the relationship with exponentials and implication. But is the syntax the cause or just a symptom? (You know what I think about syntax...) If CH could be readily applied to Java, perhaps Java's designers would have chosen a more suggestive syntax. But even if they had decided to stick anyway with C-style syntax, the idea of using abstraction to handle dependencies would have been more obvious.
Anyone knows how Scala's collections compares to C#'s linq?
Terry Tao has a nice article comparing common proofs by contradiction to its contrapositive versions: http://terrytao.wordpress.com/2010/10/18/the-no-self-defeati...
http://www.cis.upenn.edu/~bcpierce/sf/toc.html
Adam Chlipala's 'Certified Programming With Dependent Types' is a textbook about practical engineering with the Coq proof assistant. The focus is on building programs with proofs of correctness, using dependent types and scripted proof automation:
He set up the matrix of all possible integers, and started his computer stringing the primes across its surface as beads might be arranged at the intersections of a mesh. Jeserac had done this a hundred times before and it had never taught him anything. But he was fascinated by the way in which the numbers he was studying were scattered, apparently according to no laws, across the spectrum of the integers. He knew the laws of distribution that had already been discovered, but always hoped to discover more."