algorithm description thoughts: ... is pseudocode good? ever?

as far as i can see it's just "what if we made a language that isn't formally specified and isn't executable, so you just need to stare at it in order to find bugs"

like, maybe it would be nice if you could throw the wikipedia article on "binary search" into a SAT solver and prove that "yes, actually, all of these work as binary search algorithms" (and be told when they break), or something

if you implement "wrapping integers" as a type then you can even demonstrate why (Low + High) / 2 to get a midpoint is incorrect, and why you have to do Low + ((High - Low) / 2)