[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Advent of TLA+



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/d1c6ca55-7b43-4638-8ae4-b4dc40d1d327n%40googlegroups.com.