Simon Peyton-Jones: Escape from the ivory tower: the Haskell journey

> An example is not being able to prove the termination of executing arbitrary programs The theorem states that you cannot prove a program's termination any faster than running it. You're not violating any theorems. > So, Im wanting it peer reviewed. But it has been peer reviewed. Here is the publication [LINK] in this journal [LINK] > So, such methods should allow us to achieve the same amount of complexity going upward using same abstraction and shortcut techniques. First, I think you're misinterpreting (and exaggerating) what has actually been achieved. Looking at Hyper-V[1], 30KLOC of (preexisting and tested) C code have been verified in a year (out of a total of just 100KLOC), but only function-by-function, rather than global correctness properties. They wrote some global invariants, but didn't verify them. As I understand, such similar verification of various layers has been done, but no global end-to-end work. Whether low-level or high-level, there has been no composition across abstraction layers. Second, such methods would not allow us to go "upward", because there's a reason why people concentrate on the lower level. The state space is smaller there. Finally, I think you're also misinterpreting DeepSpec's work. It is at the forefront of verification of a certain kind, but if you look at their papers, when they talk about end-to-end verification, they're discussing programs that are 3KLOC C. These programs are smaller than many JavaScript libraries. Also, Coq is not

SPJ also noted that the original success of haskell was due to their pursuit of laziness. Because laziness has no place in a system with side effects, their pursuit of laziness and functional programming is what led them to discover the usefulness of monads for describing it in the first place. If they were pursuing a strict language instead, then they were allowed to take shortcuts, because sneaking in side effects is a lot easier. YEs maybe the next haskell will be strict, but getting to the point to make that decision required laziness. SPJ made a great lecture about this. It is very easy to follow and a fun insight into the academic history of modern functional languages [VIDEO]

The thing that's interesting about Haskell is that lazyness had a payoff of leading to the discovery of monad-based IO [1]. [1] [VIDEO]

That's not so simple, because large adoption at a too early stage causes the language definition to freeze before it reaches maturity. Simon Peyton-Jones from the Haskell community explaining exactly that: "What happens if [a language] become successful too quickly? You can't change anything!" [VIDEO]

Unsound typesystems are not necessarily a problem, but consider the problem the other way around: given a sound typesystem, how do we improve this in such a way that a) the average Joe will understand it b) it decreases the overhead of writing the types c) the type system helps the programmer write better programs Haskells approach to this keeps the constraint of soundness: [VIDEO] The whole video is very interesting even if you know nothing about Haskell, but are just interested in language design in general. To summarize the part of the video I just linked: Their approach so far has been to try and design the type system in such a way that you reduce programmer pain while not sacrificing soundness at all. It is a painful constraint for language designers, but it allows you to gradually add functionality to the type system from observing real world examples. The goal can be described as: Design a typesystem such that every working program can be typed in both a sound and correct way, while minimizing the amount of programs that can be typed, but are not working as intended.

> I'm from Microsoft and when you see Microsoft documentation it often says, you know, x y or z is a rich something, right. In this case Haskell - or ghc's version of haskell is a rich language. What does this mean? Sounds good, doesn't it? But it always means this, right. That it's a large, complex, poorly understood, ill documented thing that nobody understands completely. From a great talk by Simon Peyton Jones [VIDEO]

Yes, I didn't include the papers below in my parent response because, “just read these dense academic papers to understand what monads are and why Haskell has them” doesn't tend to be good advice for Haskell beginners. But learning why monads came to be included in Haskell is useful if you want to dive deeper into this stuff: Philip Wadler's original paper on Comprehending Monads [PDF]: [LINK] Philip Wadler and Simon Peyton-Jones' paper on Imperative Functional Programming [PDF]: [LINK] Simon Peyton-Jones mentions both papers and talks about why monads came to be part of Haskell in his talk on the history of Haskell here, with examples that are a little more accessible than the above papers: [VIDEO] [introduction to purity and then monads starts around 30:07] It's a funny talk and it's worth watching in full, but here's a nice soundbite: “So what did we do for IO? Well, we just didn't have any. [audience laughs] So the joy of being an academic, right, is you can design a language — in 1990, I beg to inform you — that had no input/output. A Haskell program was simply a function from string to string. That was what it was. … But this was a bit embarrassing…” He goes on to talk about other ideas they explored to create effects, why they settled on monads, and why he wishes now they had called them something like “workflows” (as F# later did[1]) to make them sound less intimidating. (Simon and Philip will both be at Haskell Exchange 2019 in London this coming week if anyone else,

That's because Haskell is like the programming language equivalent of The Gig That Changed The World[0], although I guess Algol60 also has a strong claim to that title. Let me explain by quoting these paragraphs Roger Ebert's review[1] of 24h party people: > As the film opens, Wilson is attending the first, legendary Sex Pistols concert in Manchester, England. (...) Wilson is transfixed by the Pistols as they sing "Anarchy in the U.K." and sneer at British tradition. He tells the camera that everyone in the audience will leave the room transformed and inspired, and then the camera pans to show a total of 42 people, two or three of them half-heartedly dancing in the aisles. Sounds like the average language designer entranced and inspired by their first time grokking Haskell. > Wilson features the Pistols and other bands on his Manchester TV show. Because of a ban by London TV, his show becomes the only venue for punk rock. Turns out he was right about the Pistols. They let loose something that changed rock music. And they did it in the only way that Wilson could respect, by thoroughly screwing up everything they did, and ending in bankruptcy and failure, followed by Sid Vicious' spectacular murder-suicide flameout. The Sex Pistols became successful because they failed; if they had succeeded, they would have sold out, or become diluted or commercial. I saw Johnny Rotten a few years ago at Sundance, still failing, and it made me feel proud of him. I could rephrase that last sent

Also, it's worth watching a bit of this talk (link at a particularly relevant time to start) because while Haskell is an "ivory-tower language," it is not _just_ an ivory tower language, and the people working on it are very much not just "a merry bunch of category theorists who had little interest in software engineering." [VIDEO] This talk is seven years old btw. Caring about industry users in Haskell is not new.