[tlaplus] Re: Advent of TLA+

[Andrew Helwer <andrew.helwer@xxxxxxxxx>]

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

On Wednesday, December 13, 2023 at 9:16:16 AM UTC-5 Murat Demirbas wrote:

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

On Wednesday, December 13, 2023 at 8:27:38 AM UTC-5 Murat Demirbas wrote:

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

-- 
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4d0ef92c-3d33-43b5-b903-9e1795bece93n%40googlegroups.com.