Serokell Blog

For us, there were a couple advantages. For context, I work at FOSSA (https://fossa.com/). Our core product solves software supply chain needs in enterprises (around licensing and security), and our core technology is around compiler, build, and source code analysis.

Off the top of my head, 3 advantages stood out:

1. First, if you're not going that far off the beaten low-level path, Haskell has incredible productivity benefits. Effect tracking has enormous benefits for testability and understandability. If you've ever been down a debugging rabbit hole shaped like "there's no way this logging call is sending that API request", then you might be pleasantly surprised to discover that you can statically guarantee that this doesn't occur in Haskell programs! Pattern matching, algebraic data types (sum types!), and typeclass derivation make it much easier to make it impossible to construct invalid representations of data. Other languages are finally picking this up, but their versions of pattern matching often have caveats for backwards-idiom-compatibility. And monads are a very powerful abstraction. It's like being able to write your own semantics for async-await (I've talked more about this before at https://lobste.rs/s/7cllte/monads_part_six_really_what_is_monad#c_nbusni).

2. Haskell was a good domain fit for us. One thing we build is the FOSSA CLI (https://github.com/fossas/fossa-cli/), which runs in customer CI pipelines to analyze their builds. It's a very compiler-shaped…

Thanks for your comments. There does seem to be three languages sure to engender disparate opinions: Lisp, Prolog, and Haskell. I suppose that their advocates can be forgiven for their enthusiasm. They are all quite remarkable languages.

I am unqualified to assess the benefits of an advanced type system, after all, I've only worked through examples in a few Haskell books. I've never used Haskell professionally. Haskell is a lovely language. Its compiler is a remarkable achievement of computer science, mathematics, and engineering. Simon Payton Jones deserves the notable accolades and awards that he as received.

In my opinion, Haskell's most important contribution is in pushing the state of the art of programming languages forward. Is it practical? Yes, that too, but after all these years, it hasn't really become popular because being "practical" wasn't the main goal for Haskell. Haskell was designed to explore the non-strict functional landscape. Haskell's designers made good choices and were able to expand our understanding of non-strict functional programming (e.g. see Miranda [1]).

In the past I did years of research in program verification, so I'm naturally skeptical of the widely repeated claim that "Once your code compiles it usually works" (it's even on the haskell.org site). In what universe is this true? Verification that a program meets its specifications is quite difficult. In general, no compiler for Haskell can even verify that a program will terminate (the…

This is actually a very good comment. Haskell has had these features since early ~2000s and it was a major competitive advantage in the language space, but today I would argue that if you're using a modern language then they don't stand out as much. Nevertheless, not all popular languages provide all the above mentioned features and in case they implement them it's usually in a compromised fashion. For example, nullable types are still an open issue in Java, while C# and Typescript provide easy ways to circumvent them, a lot of times by accident (the main issue is that they're mostly annotations, not runtime checks).

On the other hand, you mention several features which Haskell provides, usually through libraries that can only be implemented due to the features provided by the base language:

- Refinement types [1] allow to add runtime invariants to existing types in an ergonomic fashion, or you can go even further and use something like LiquidHaskell[2] to enforce properties at compile time.

- For multithreaded programs, the existence of STM[3] allows to to write mutable variables which are safe to use across threads. Very few languages offer something like this.

- For structural dependencies, you can apply the techniques of "ghost of departed proofs"[4]. Personally I don't like to go that route since programming becomes an act of "proving" rather than "doing" but I appreciate the fact that you can encode it if you want/need to.

- Metaprogramming in Haskell is not as…

> read this: https://serokell.io/blog/dimensions-and-haskell-introduction , then look into the referenced libraries.

Dude, I actually work with dependent type proof assistants (Lean), with a HOL proof assistants (Why3), and FOL/ZFC proof assistant (TLA+'s TLAPS), as well as with a model checker for TLA+ (TLC); I've also worked with a model checker for Java in the past. I have read several books on the subject, and have written two (both available online: https://pron.github.io/tlaplus, and https://pron.github.io/computation-logic-algebra). I've also trained engineers in formal methods.

> Have fun arguing with objective reality.

You've read a few blog posts on one aspect of one formal method, and seem to have not even heard of the majority of software correctness research. You certainly don't seem to have practiced formal methods in industry even using one method, let alone more than one. You don't even seem to know what first-order logic is, what higher-order logic is, and I'm sure that if I asked you the difference between HOL and Martin-Löf type theory, or between classical and constructive mathematics you won't even know what I'm talking about; ditto if I asked you what it means for a type theory to have a set-theoretical interpretation (as Lean's, and maybe Agda's -- I don't know -- type theories do). You've read a few blog posts about a small part of one of the most complex, refractory topics in all of computer science and software engineering. You don't know what…

>It doesn't, though.

read this: https://serokell.io/blog/dimensions-and-haskell-introduction , then look into the referenced libraries.

Have fun arguing with objective reality.

As for resource safety, Haskell is yet to follow Rust and introduce linear types, but many cases are covered by bracket pattern https://wiki.haskell.org/Bracket_pattern which can be enforced on type level using some tricks with ST monad. BTW, it is very similar to RAI discipline suggested by many C++ guidelines, but here it can be enforced.

Again, have fun arguing with objective reality.

>This is true for all formal methods, but here, too, most of them beat deductive proofs.

Sure, feel free to feel superior about that. The problem is, again, type system can be embedded into programming language and allow for quite a bit of guarantees even without full blown dependent types. Java has static typing for a reason.

Sure, to enforce some properties using type system we need an uncomfortably deep delve into type theory or use awkwardly polymorphic code. However, a lot of properties can be enforced with relatively low cost, and Haskell is a long-running research project on what properties are practical to enforce this way.

So, why I need to use proof assistants for properties that can be enforced via practical type system? I really don't see a reason.

> The compiler and the build system have gotten a lot more stable over the past several years.

GHC2021 promises backwards compatibility, but it includes ill-specified extensions like ScopedTypeVariables. TypeAbstractions were just added, and they do the same thing, but differently.[0] It hasn't even been decided yet which extensions are stable[1], yet GHC2021 still promises compatibility in future compiler versions. So either, you'll have GHC retain inferior semantics because of backwards compatibility, or multiple ways of doing the same thing.

GHC2024 goes even further and includes extensions that are even more unstable, like DataKinds.

Another sign of instability is the fact that GHC 9.4 is still the recommended[2] release even though there are three newer 'stable' GHCs. I don't know of other languages where the recommendation is so far behind! GHC 9.4.1 is from Aug 2022.

It was the same situation with Cabal, it took forever to move beyond Cabal 3.6 because the subsequent releases had bugs.[3]

[0]: https://serokell.io/blog/ghc-dependent-types-in-haskell-3 [1]: https://github.com/ghc-proposals/ghc-proposals/pull/669 [2]: https://github.com/haskell/ghcup-metadata/issues/220 [3]: https://github.com/haskell/ghcup-metadata/issues/40