I've only dipped very shallowly into TLA+ and haven't had time to investigate, but I have been wondering if we can leverage Haskell's type system to make sure w

I've only dipped very shallowly into TLA+ and haven't had time to investigate, but I have been wondering if we can leverage Haskell's type system to make sure we're matching the abstractions we've assumed for TLA+ at a low cognitive overhead.