/advent-of-tla

AoC goals in TLA+

Primary LanguageTLAMIT LicenseMIT

Advent of TLA+

Advent of Code are popular computer programming challenges, which can be solved in every programming language. But this repository makes a different take on AoC problems: instead of solving them, it formally specifies their goals using TLA+.

For some kind of problems, it's hard to write a spefication that does not look awfully a lot like a solution. It's important to remind that in general case a specification is very different from code, and it has a different purpose.

Specification of parsing is deliberately ommited. For this reason, there's no specification for day 4 of AoC 2020.