Advent of TLA+

[Murat Demirbas]

How much effort would it be to create an Advent of TLA+ for next December?

Can we get people in our community excited to prepare 25 modeling puzzles (as part of a running narrative) and deploy this as a website like the Advent of Code?

https://adventofcode.com/

I think this would be a huge boost for TLA+'s popularity and adoption. We need to be very intentional about the kind of modeling problems we choose. They should be close to the distributed systems primitives so people see the practical usefulness of TLA+ for real systems. But they should also be fun, and the counterexample should be the solution they need to enter to advance to the next state in the puzzle/modeling narrative.

I think this is worth brainstorming on. I would be interested in meeting people online first, and maybe then as a working group at the North America TLA+ conf.

Best wishes,

Murat

[Murat Demirbas]

Maybe a Rustlings style learning environment would be more instructive and more closely aligned with distributed/concurrent system modeling, but I think there is an advantage to the real-time/campaign/fun/social feeling of Advent of Code.

https://github.com/rust-lang/rustlings

[Andrew Helwer]

This is a good idea but it takes a lot of work to make the puzzles. Apparently the guy organizing AoC works on it for four months.

I agree that a rustlings-style series of exercises is a great way to learn languages. I also like The Natural Number Game (for Lean) for this.

Creating a series of online exercises of this type was an early goal of my rust-based rewrite of SANY/TLC which is on the backburner for now. Perhaps next year I will finish it.

Andrew

[Maroš Orsák]

+1 for this. I think that´s a great idea . 😊

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4d0ef92c-3d33-43b5-b903-9e1795bece93n%40googlegroups.com.

[Markus Kuppe]

I don't believe we are blocked on *online* exercises, considering that even rustlings requires a local installation or a Gitpod cloud workspace [1]. And we've already created cloud workspaces [2,3] for all of our tools: TLC, Apalache, and TLAPS [4]. Also, don't we actually want potential users to install our tools locally?

In terms of exercises, our example repository is full of easy-to-hard specifications. More concretely, the Blocking Queue [5], EWD840 [6], and the EWD998 examples [7] at least share a similar structure with rustlings, meaning they form a sequence of loosely dependent commits and are designed as hands-on excercises within an IDE. Apalache also has a nice tutorial [8].

I would argue that we already have all the pieces; what we lack is a consistent and unified presentation.

Markus

[1] https://github.com/rust-lang/rustlings?tab=readme-ov-file#getting-started
[2] https://gitpod.io/#https://github.com/tlaplus/examples/
[3] https://github.com/codespaces/new?hide_repo_select=true&ref=master&repo=52869867&skip_quickstart=true
[4] https://github.com/tlaplus/Examples/blob/master/.devcontainer/install.sh
[5] https://github.com/lemmy/BlockingQueue/?tab=readme-ov-file#v01-java-and-c-implementations-with-configuration-p4c3b3
[6] https://github.com/lemmy/ewd840/commits/main/
[7] https://github.com/tlaplus-workshops/ewd998/commits/main/?after=f9475107b80d58b3a36cf239e3991a9fa7dcf6bd+69
[8] https://github.com/informalsystems/tla-apalache-workshop?tab=readme-ov-file#thinking-about-protocols-with-tla-and-apalache
[8] https://github.com/informalsystems/tla-apalache-workshop?tab=readme-ov-file#thinking-about-protocols-with-tla-and-apalache

[Samuel Miller]

I’d be interested in helping. This was on Hacker News today. “Advent of Distributed Systems” using Go. 

https://aods.cryingpotato.com

A weekly challenge would be more manageable (vs daily) and also help bridge the gap noted by many for intermediate learning material. 

I’ve also been thinking that “teaching distributed systems with TLA+” may be more interesting to a wider audience than “teaching TLA+ with distributed systems.” Software Foundations teaches programming language theory with Coq, so it gets wide exposure for general students as well as people who want to learn Coq. May be an approach worth considering. 

--

[Hillel Wayne]

I think an easier alternative would be to do a series of essays on TLA+, like vim and raku do. Definitely less work!

H

--

[Hillel Wayne]

Examples:

https://efertone.me/series/advent-of-vim-2021/

https://raku-advent.blog/