Hacker News Reader

> validating the utility of those abstractions on their "rigorous mathematical foundations"

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.

[1]: https://en.wikipedia.org/wiki/Monad_(category_theory)

>It could be argued that once a person learns these concepts they are given a better means of reasoning about programs than other languages,

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.

The gain from maths is that you can tell everyone what an exalted, rarefied experience you are having writing the same programs people write in blub, except more slowly, somehow using elite stuff you know from maths.

edit: I have no criticism of maths here, maths is great.

> which makes them easier to reason about

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.

>I like to keep my abstractions cognitively simple (primitive, even), and my algorithms sophisticated and powerful.

This is extremely poor programming practice. Let me guess, you're a solo developer and/or working on a tiny team.

At the moment I have a small team, but before that I was CTO of a large team working on real time (soft and hard) defense systems.

> Easier to reason about by whom?

As I said, by those who are aware of the math concepts they are based on. Monads are I think the best example for Haskell; particularly in how they behave with respect to functions, which fits quite nicely with a categorical point of view.

> I think that Haskell is better if you are mathematically minded and interested in thinking (a lot!) about abstractions.

I'm not sure you can be mathematically minded in the pure mathematics sense (which is what Haskell draws on) without being interested in thinking a lot about abstractions. If you are more focused on concrete mathematics, then Haskell is unlikely to be your ideal language, but when people reference mathematics in regards to the language I suspect they are referring to the pure variant. In any case, I am, which is I think most of the confusion here.

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

The only built in formal verification I can think of in Haskell is the type system. In that case, I think your analogy breaks down; I'm not sure how one can manage to program (effectively) in any language without understanding its type system. If you are referring to an external static analysis tool, then I'm not sure how you can put that on Haskell itself.

> a language designed to make a machine's reasoning easier would also do the same for a human

I believe it does for humans who come from a pure math background, in the same way programmers who know an object oriented language will find it easier to grasp another object oriented language. Moreover, it seems pretty clear that this is no a coincidence; it was the driving force behind Haskell's most fundamental design (e.g. Curry Howard) and its library (e.g. monads). So if you (as you say) are not interested in abstract mathematics, then it is no wonder you don't care for its methods.

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

Unless, of course, they are focusing on humans that are not only well versed and comfortable with certain branches of math, but prefer that mode of thinking. Haskell's unofficial motto of "avoid success at all costs" makes me think that focusing on this demographic is likely one of the language's design features, as opposed to making the best language ever for everybody. In any case, I would argue it is good for mathematicians, but not that all of the effort to move to that way of thinking is something universally useful for programmers.

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

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.

> 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 news to me! Mathematicians wouldn't find the monads that appear in Haskell especially interesting, I think (at least not the ones that are instances of `Monad`), but that's beside the point.

So I'm repeating what somebody said rather than my own claim, but I think it was that Haskell monads didn't have to be... one of left- or right-associative. But they had to be the other.

Wish I knew of a good way to search HN; it was in a comment here maybe 6 months or a year ago...

> Haskell monads didn't have to be... one of left- or right-associative. But they had to be the other.

That's very puzzling. I wish I knew what you were referring to!

Hah! Found it.

https://news.ycombinator.com/item?id=7770129

That was my source (I was the parent). Unfortunately, it doesn't quite answer your question...

If that Haskeller you're referring to was me then I'd like to clarify: I think mathematics is a good fit for humans because it's the output of a few centuries of careful large scale use and design, not because it's simpler by any direct merit.

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.

No, it wasn't you :)

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.

Where is this strange obsession with Curry-Howard coming from? It's not a practical issue, with regard to verification or otherwise, and the Haskell world in general doesn't try to claim it's one. It's just an interesting symmetry, that's all.

What I mean by that is the philosophy that verification should be based on explicit types in the original program source. This intricately ties the process of authoring software with that of verifying it. The result is needlessly constraining both the developer and the verifier. It only lets you (easily) write code within what it can prove, and only lets you prove properties that can be expressed by the types that you use.

Other approaches say, we'll let people write code however they feel most comfortable doing (more or less), using types whose expressivity is defined not by the limits of the verifier but only by various concerns over language complexity, mental overhead, performance and teamwork, while we let the verifier prove whatever types it can. If it proves that the variable x is of type "an integer which is always equal to the current time in seconds modulo seven, except on Saturdays when it's always zero", then that's great!

I think given your clarification here I can directly state that (a) I don't think this is necessary and (b) I don't think C-H is a good name for this exactly. Point (b) is a bit silly to discuss, but point (a) is key.

I think there are workflow and ux efficiencies for having the compiler reject programs which are poorly typed. This typing can arise from either internal or external verifications for all I care, but the ergonomics of each vary a lot as well.

I think for both practical and ergonomic reasons, completely automated proofs are weak. There's no reason not to run them if you agree with the validity and importance of the theorem they represent, but by their nature the meaning and effectiveness is highly limited.

By having your proving language align with your programming language you sidestep this issue by forcing everyone's hand into revealing their intentions to the verifier. From a process perspective, this keeps people from cheating ("whip and bondage and all that") and it also, more imprtantly encourages the code author to tell a complete story of what they're doing instead of merely creating the artifact. This is great for the more "conversational" style of proving that occurs with things like Agda, Coq, Epigram.

External proofs can act similarly but I think your examples are often really archaic. It seems to me that I nteresting theorems must be derived alongside your program be they internal or external. JonPRL is an interesting demonstration of this method (as is NuPRL, but you can't really access that one).

> forcing everyone's hand into revealing their intentions to the verifier

Only those intentions which the verifier can prove. Want a stronger verifier? You need to change the language.

> encourages the code author to tell a complete story of what they're doing instead of merely creating the artifact

But it's not a complete story. Haskell's type system can't express some of the most interesting bits of the story. I find it ironic that Haskell's type system can't even verify the validity of monads (I mean compliance with the monad laws)...

> External proofs can act similarly but I think your examples are often really archaic.

I don't know if they're archaic, but I do know that Amazon uses TLA+ to verify their Java code (and TLA+ is somewhat similar to Esterel's verifier)

Well, phew! ;)

To the first point: I'm happy to generalize my claim outside of merely C-H school (which I'd call the "logical" school, maybe this is the same or maybe it's more broad than what you mean by C-H) and make a mere subclaim that the logical school will prevail.

To the second point: I think there's plenty of existing empirical results, but not direct ones. E.g., how many advanced physicists today are using their own, highly divergent language for writing their theories (not their code, notably).

I think the direct empirical results—like the one you claim and I'd, without verification, buy—are conflated with technological progress and desire to get things done over getting them done consistently or well.

> make a mere subclaim that the logical school will prevail.

I'm not entirely sure what you mean, but if you mean that programmers will write code in languages that are directly tied to logical proofs (through the type system), then I'll take that bet.

> E.g., how many advanced physicists today are using their own, highly divergent language for writing their theories (not their code, notably).

Writing programs is not (or no longer) a scientific endeavor. I think software development is much more similar to the work of an architect. Some crucial parts can and must be verified sufficiently, others may have different MTBF requirements, other aspects are just aesthetic, very often you need to cut corners to meet budget and time requirements, and above all, your approach must be pragmatic and take into consideration that the building will need to be maintained and renovated by people other than you -- people with varying qualifications -- long after you've moved on to other projects.

> desire to get things done over getting them done consistently or well.

Perhaps, but what makes you think this desire will change? (I don't think it should change, but that's a different issue)

The bet is on, then, I suppose :)

I think your point about architecture versus science is a good thing to think about. On one end, I agree with everything you're saying. On the other end, I see that architecture only works due to a large set of bombproof civil engineering practices employed both in the past to lay down the principles of architecture and continuously to validate that the work of the architects won't kill anyone.

My understanding is that these people are crucial to the success of any architecture project.

So with that I might ask whether the foundations for CS have been laid and whether the built-in civil engineers we employ are sufficiently able to do their jobs.

There is an immediate question as to whether we should care... and I'll just wave that aside for the moment since I have as least an aesthetic horse in the race that we should care.

After that we might ask if the founders of modern CS have done a sufficient job laying their foundations so we can use them. I'd believe there is some significant debate about whether this is true (Dijkstra would argue we're not even close, is my guess).

I'm willing to put a little, conservative bet on the idea that even if the "founders" all agreed their work was done that they'd be wrong, too. I just think this field is too young.

I thought about exactly that as I was writing the analogy, and I just don't know... :)

I do think, though, that just like with architecture, different components require different care, and those that require absolute correctness are a rather small part. I also think that math (as in architecture) is only a very small part of the solution. It's essential, but it doesn't dictate the path of the project, and in the end most of it is just a lot of knowledge of how people behave (the people who live or work in the building and the people who will run, clean and maintain it).

P.S.

I do, however, believe in the combination of familiar "cognitive" languages alongside verification tools. For example, see how Amazon uses TLA+ to verify their Java programs[1]. This alone is more real-world usage than Haskell has ever seen.

[1]: http://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-s...

I think you're pointing out the difference between the "art" and "science" of architecture. A similar thing arises, IMO, in technical products between product and technology. There's a whole hell of a lot of psychology on the product side, and I think there always will be. Constrained by some artificial line to the technology side, I take my bet that mathematical tendencies will dominate.

It was me[1] and I'm afraid you are still mistaken on a number of points:

> The truth is that Haskell -- like all programming language -- has made a design choice, which was to bake in correctness proofs based on the Curry-Howard correspondence into the language

Haskell is not a logic and is not used to write proofs for program verification. General-purpose functional languages don't have all that much to do with CH, and they don't include any design decisions that favors a particular approach to verification. The type system helps you enforce useful invariants in your code and can make verification easier, but it's completely orthogonal to how you can prove programs correct.

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

Theorem provers based on C-H are general-purpose logics that can be used for a lot more than just program verification. So, different tools for a different purpose. Having said that, they have proven to be very useful for verification of complex systems like those you listed, where existing tools have trouble even stating what correctness means. That is, they can help us answer the question "how can we be certain that this compiler, verification system, etc. is correct?" That typically includes representing your object language in your theorem prover and proving things about the language, which is quite different than showing that an algorithm meets some specification.

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

You can show that, quite literally, any "true property" of a program in your more complicated language is also true of the corresponding program in your simpler language. So, if you come to some correct conclusion, even if the way you reason is completely bogus and just happens to work, it will be valid for your simpler language.

There's no need to solve the much, much harder (and poorly specified) problem of "what is easiest for humans". That's not to say that the current crop of functional languages is presented in the easiest way for people to understand, but that's an entirely different problem independent of semantic considerations.

[1] https://www.reddit.com/r/programming/comments/3i1l9n/from_im...

> It was me

Yes, it was you :)

> The type system helps you enforce useful invariants in your code and can make verification easier, but it's completely orthogonal to how you can prove programs correct.

That's true for Java. Haskell, OTOH, constructs the entire language around verification through types and pure functions, and everything else is secondary. I don't know if the connection to C-H was made later or was a conscious design decision, but the result is the same from the user's perspective.

> Theorem provers based on C-H are general-purpose logics that can be used for a lot more than just program verification

We've discussed this before, and I believe those uses are too niche for the Haskell approach to gain any significant traction.

> You can show that, quite literally, any "true property" of a program in your more complicated language is also true of the corresponding program in your simpler language.

Of course, but that is only useful if a human programmer writing in the more "complicated" (by your definition) language would use the "simpler" subset, which, by my definition, she wouldn't do.

> There's no need to solve the much, much harder (and poorly specified) problem of "what is easiest for humans".

It's not a mathematical problem with a clear solution, and therefore requires no robust specification -- just like architecture (of buildings), or any other UI design problem. We learn what works through trial and error and try to do better.

I find it hard to accept the point of view which considers UI to be a methematical puzzle, or, alternatively, that doesn't recognize programming languages as UIs.

> but that's an entirely different problem independent of semantic considerations.

From a UI design perspective, you can't separate the two, because if the user fails to interact with the machine well, you don't know if it's a matter of design or presentation unless you empirically test it.

> That's true for Java. Haskell, OTOH, constructs the entire language around verification through types and pure functions, and everything else is secondary. I don't know if the connection to C-H was made later or was a conscious design decision, but the result is the same from the user's perspective.

The type system of Haskell is far more interesting and powerful than that of Java, but I think you're overstating the difference. While Haskell's type system does allow you to do a few more things than just demonstrate restraints on your code (such as construct more expressive types and make use of type classes and polymorphism), at the end of the day the overwhelming utility of the type system is being able to more easily make guarantees about your code, just as it is in Java.

Curry-Howard only really becomes interesting once you have dependent types, and only becomes bullet-proof when your language is total. Haskell has neither property. The connection to C-H is something which might interest a large subset of Haskell programmers (who would likely take that interest into a study of Coq, Agda or Idris), but it has pretty much no bearing on the day-to-day usage of Haskell.

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.

-

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.

I don't think the connection between Haskell and Curry-Howard is that strong (it's stronger since GADTs were added, but still, functions are not even terminating). Rather, I think the main thing that makes Haskell "mathematical" and easy to reason about is that it is pure, so you can reason about things equationally.

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.