Hacker News Reader

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.