@InfiniteNutshell@mastodon.social
Post #1823388
2026-04-25 13:50 UTC
@lindsey interesting! what makes it desirable for definitions like this to include or exclude trivial cases? my intuition is that you should be able to satisfy safety properties by just always rejecting the input; not sure about liveness but maybe it's the opposite?
Replies (1)
-
@lindsey@recurse.social 2026-04-25 16:48
@InfiniteNutshell Usually there's an implementation that's trivially safe or trivially live, so either by itself is not that useful. You want it to be both, if possible (though in distributed systems this is often impossible). It's desirable to exclude trivial cases because if you say "we showed that our implementation is safe and live", you want that to really mean something, you know?