Oh man. If you like math, CT gives nice mathematical definitions for stuff. I would love to use my algebra skills to do general programming like I can use my linear algebra knowledge in numerical programming.
I'm making bold claim that I hope someone can debunk with awesome counterexamples:
"CT HAS ZERO APPLICABILITY IN PROGRAMMING"
Using CT to Linear algebra analogy: CT in programming is like learning definitions of vector spaces, subspaces, span, and basis and stopping there. No CT equivalent for solving linear systems, linear transformations, least-squares or eigenvalues. Just because you have rooted programming in cool algebraic notation does not mean anything in itself.
Another trick Haskell uses is preferring abstractions that are based on concepts from CT[2], and validating the utility of those abstractions on their "rigorous mathematical foundations". This is again just another case of taking you to the math rather than the other way around. Programming languages are first and foremost human languages, meant to be written and read by humans. As such, their power is drawn from a single source: their interaction with human cognition. Whether an abstraction is "mathematical" (whatever that means) has absolutely no relevance to its power, which comes from cognition (and psychology in general) rather than math. All this "in your face" math does is make the machine's job of verifying your software easier.
A Haskeller tried convincing me that such a language is a good fit for human programmers, too, because all it is is a subset of more traditional, impure languages. But the notion of subset => simpler is a mathematical notion with no relevance to cognition. If humans operated in this way, natural languages would have been much more mathematically simpler, too.
[1]: See KeY: http://www.key-project.org/
[2]: To be fair, I'm not sure that Haskell, given its original design philosophy, has much choice in the matter.
Some Haskell users may think this, but I think the usefulness of the foundations is not derived from rigor. Instead, it is derived from the wealth of knowledge we have about mathematical structures which makes them easier to reason about. So by linking the programming structures you are using (e.g. monads) with associated mathematical structures (also called monads[1]), all of the mathematical knowledge surrounding that structure suddenly becomes available. This is rather like how doing numerical calculations with matrices benefits from the wealth of knowledge about linear algebra.
Another "mathy" aspect that Haskell and similar languages have is that they like to start with a few fundamental constructs and build everything else within that system. This is more a design philosophy than anything, but I think it does have its advantages in that it results in better composablility, since everything "comes from the same place".
As far as the relationship to cognition, I think Haskell will be better in this regard if you are mathematically minded, because you will understand programming constructs from their mathematical roots. For example, I had an easy time picking up monads because I knew the category theory version. It could be argued that once a person learns these concepts they are given a better means of reasoning about programs than other languages, but I suspect that largely depends on one's intellectual leanings.
This was my challenge. Give concrete examples where you reason about programs better while programming because of the category theory. People have been arguing this for years without any concrete examples. I'm a math person and I would really like to use category theory and mathematical intuition when programming.
I argue that there is very little usable structure for reasoning for the programmers after the definitions. There is no buildup of structure that is common when mathematics is used effectively. The gain from math is very small or nonexistent.
Easier to reason about by whom? Most programming models have their own calculi which are exploited by their respective verification tools. They don't, however, expose that to the developer.
> I think Haskell will be better in this regard if you are mathematically minded
I think that Haskell is better if you are mathematically minded and interested in thinking (a lot!) about abstractions. I like to keep my abstractions cognitively simple (primitive, even), and my algorithms sophisticated and powerful. I'd rather the people writing the verifier put their mathematical leanings to use on the relevant calculus, while I use mine on the algorithmic domain I'm working in.
Just like I don't require the developer using my database to be familiar with data structures and concurrency, I don't want those interested in formal verification requiring me to change my programming style to make their job easier. In fact, their job is quite the opposite: provide verification tools that are useful for the programming languages that make for a good cognitive fit, rather than design languages that make verification easier with the (possibly misplaced) hope that by some unexplained coincidence, a language designed to make a machine's reasoning easier would also do the same for a human.
Software verification is a fascinating algorithmic topic. Language design is a fascinating UI endeavour tasked -- like all UI -- with coming up with great cognitive abstractions. The two should, of course, cross-pollinate one another, but shouldn't become the same. Language designers should spend their time thinking how humans think about computation and how they interact with computers, not how to make programming models fit certain branches of math.
Only if what the language does with monads exactly mirrors what CT does with monads. Otherwise the language subtly lies to you.
In fact, this may be the case. I seem to recall that Haskell monads only have to obey two of the three monad laws. That is, they don't have to truly be (CT) monads. That's supposed to not matter, but if nothing else, it kind of makes your argument a bit less well grounded.
> This is rather like how doing numerical calculations with matrices benefits from the wealth of knowledge about linear algebra.
In the exact same way, this is only true if the matrix package truly implements linear algebra correctly. To the degree that the matrix package doesn't do that, your reasoning based on linear algebra leads you astray.
Human languages might then be said to be the process of an even longer historical evolutionary process—so they must be the best, right? My thoughts here are that the natural selection pressures of human languages are very different than that of mathematical languages and we should direct the conversation there.
Mathematics expresses a desire for (a) elegance and (b) economy of proof which might be taken to be an expression of the complete logic of a complex idea. This isn't the perfect thing to optimize for, but I think it's well in-line with what we're doing in programming.
So I tend to take the bet that in the long run PLs and mathematics will converge and PLs will have further to move than the bulk of modern mathematical literature.
I have two issues with your argument. The first is the (implied, I think) assumption that C-H is the only way to apply math to programming languages. I think C-H has so far disappointed, because 1., people don't seem to want it, and 2. because other verification systems (like KeY) or the verifiable imperative, reactive real-time languages of the eighties (like Esterel) whose descendants are still in use today, have so far been used to much better effect.
The second is the assumption that by virtue of being well-studied an academic field would somehow prove a good fit with human psychology. That demands some empirical results which, again, are so far very disappointing.
> So I tend to take the bet that in the long run PLs and mathematics will converge
If by that you mean that the C-H approach will win, I'm happy to take that bet.
I believe that over the past 15 years, the relative usage of Haskell by developers has only decreased (the number of people using Haskell has grown less than the total growth in the number of programmers, much due to JavaScript and the web), and even though I could be wrong about that (I basically made it up :)), it's not too far from the truth.
Don't get me wrong, there are certainly academic influences (coming from C-H languages) on mainstream, or hopefully-mainstream languages (Rust is a clear example), but I don't see any signs of a trend towards adopting C-H as a basic language design philosophy.
-
I totally agree on this point and I've tried my hand at Haskell several times only to find myself going to some other language like F#, OCaml, or Common Lisp. It just feels too 'stiff' in terms of a programming language. I can't seem to write in it without running into its limitations (Not strictness. I can handle strictness in a language.). When I write a program I think about what I have to pull data from and what the data should become along the way. Even if parts of my program will be standardized into a library for a project I still like being able to get it setup in such a way that I can modify it easily. Haskell doesn't seem to let me do that without redoing the entire function signatures and sometimes due to the notation the signatures don't fit the data well if at all.
That will help verification no matter what framework you are using. For example, look at the seL4 verification. That was done in Isabelle/HOL, so it doesn't use Curry-Howard in any way. But even so, they proceeded by writing two versions of the operating system, one in C, and one in Haskell to make it easier to reason about.
The epiphany I had from this is that, while linear algebra's utility comes in the form of designing efficient algorithms, CT's utility (in Haskell) comes in the form of understanding structures. It's similar to thinking of modular arithmetic in terms of remainders vs. quotient groups. I get lost doing anything complex with the former way of thinking, but when I switch to thinking in terms of basic abstract algebra suddenly the foliage clears and the way ahead is clear.
Category theory is a language created to communicate complex models. If it's not obvious yet that you can't use CT the same way you use algebra, let me state so: you can't. CT must be less powerful than algebra, because you can't reason about complex stuff as easily as you can reason about simple stuff.
Yet, one mostly can not write a program nowadays without using CT. There's no language that does not implement a subset of it. You don't notice it for the same reason that fish do not notice the water.
But as powerless as CT must be, it gives you plenty of tools for simplifying your models, and not having those tools available can only make your program more complex, never simpler.
