Maelstrom: A workbench for learning distributed systems

I'd start by reading the papers mentioned below and then implementing a real distributed kv store without any fluff, just hard code your test cases into a simple client. Then try load testing by running a ton of your client. The problems you run into will be practical and real and you will have to debug them yourself with real tools. Then after that basic exercise I think Maelstrom will be more useful to you. TLA+ is an awesome design tool but imo implementation practice is more helpful for a beginner, you'll be more familiar with the problems TLA+ can help you solve.

https://omscs.gatech.edu/cs-6210-advanced-operating-systems

I suppose because Jepsen is written in Clojure. And that is probably because the author was versed in Clojure and that is the language he picked.

At the end of the day a Clojure program is a .jar file. You can write your systems in any language and this will command them. But Clojure is a very cool language worth exploring.

Why do astronauts wear space suits?

I feel this in my newcomer bones. Every time someone badass writes something in erlang or clojure or rust or something and I'm like... "the problem was complicated enough, why'd you add an esoteric language to it?"

Slightly off-topic, but I have worked with another tool by the author (Jepsen), which is also written in Clojure and in fact a Clojure library. I'm fairly proficient with functional programming in general, but had never touched Clojure before. My experience working with Jepsen was quite frustrating simply because of the fact that it's a Clojure library. Clojure is dynamically typed and it happened fairly frequently that I had to dig into Jepsen's source code simply because some type errors were only caught very deep in the call stack. Jepsen itself is a really great tool and I'm a very big fan of it's creator (Kyle Kingsbury), but the fact that you can only use it through Clojure is kind of sad. I guess it gets better with more clojure experience, but a dynamically typed functional programming language is kind of too much of design flaw for me to want to invest more time in the language.

Maelstrom is a frontend to Jepsen, a Clojure library for testing concurrent systems--mostly databases. Jepsen is also written in Clojure and Java--both run on the JVM.

Because it tests concurrent systems, the language itself needs good support for concurrency. Clojure's persistent data structures make it easier to write correct concurrent programs, and the language and runtime have excellent concurrency support. I also considered languages (like Haskell) with more rigorous control over side effects, but decided that Clojure's less-dogmatic approach was preferable.

Because Jepsen tests databases, it needs broad client support. Almost every database has a JVM client, and Clojure has decent Java interop.

Because testing is experimental work, I needed a language which was concise, adaptable, and well-suited to prototyping. Clojure's concision and syntactic flexibility work well for that.

Tests involve representing, transforming, and inspecting complex, nested data structures. Clojure's data structures and standard library functions are possibly the best I've ever seen. I also print a lot of structures to the console and files: Clojure's data syntax (EDN) is fantastic for this.

Because tests involve manipulating a decent, but not huge, chunk of data, I needed a language with "good enough" performance. Clojure's certainly not the fastest language out there, but idiomatic Clojure is usually within an order of magnitude or two of Java, and I can shave off the difference where critical. The JVM has excellent profiling tools, and these work well with Clojure.

Jepsen's (gosh) about a decade old now: I wanted a language with a mature core and emphasis on stability. Clojure is remarkably stable, both in terms of JVM target and the language itself. Libraries don't "rot" anywhere near as quickly as in Scala or Ruby.

Clojure does have significant drawbacks. It has a small engineering community and no (broadly-accepted, successful) static typing system. Both of these would constrain a large team, but Jepsen's maintained and used by only 1-3 people at a time. Working with JVM primitives can be frustrating without dropping to Java; I do this on occasion. Some aspects of the polymorphism system are lacking, but these can be worked around with libraries. The error messages are terrible. I have no apologetics for this. ;-)

I prototyped Jepsen in a few different languages before settling on Clojure. A decade in, I think it was a pretty good tradeoff.