Post #1823370

2026-04-23 21:28 UTC

I guess we also need some sort of non-triviality criterion like "doesn't always produce the same snapshot", kind of like how the validity criterion for consensus algorithms rules out algorithms that ignore their input and always decide on the same value

Replies (3)

@elb@social.sdf.org 2026-04-24 00:40

@lindsey I was just talking about this kind of thing with @akhirsch at lunch yesterday. I'm super proud of your student for noticing that, what I was specifically musing on is that I find it difficult to teach students to find trivial solutions even when prompted. (I think this is similar to finding corner cases and limits; it requires an inversion of thinking that takes some practice!)

Open ##1823375
@jer_gib@functional.cafe 2026-04-24 02:08

@lindsey Without having seen your definitions, wouldn't something like "eventually captures the entire state" be a necessary part of correctness?

Open ##1823376
@InfiniteNutshell@mastodon.social 2026-04-25 13:50

@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?

Open ##1823388