Now you're making me think about my specification and verification professor from years ago. A lot of the exercises had us specify stuff with some formalism. So

Now you're making me think about my specification and verification professor from years ago. A lot of the exercises had us specify stuff with some formalism. Something like a finite state machine for a 3 digit combination lock, or pre- and post conditions of algorithms, loops and such. The tutorials about these exercises were really cool, because we'd spend a short time wrapping up mistakes in the notation. But then he usually classified and grouped the different solutions according to the design decisions made and it would evolve into large discussions about tradeoffs of choices. Someone might go "Well I figured the FSM would be smaller if I fail on the first wrong number, and it'd be user friendly because it fails early", and someone objects "But that's insecure!" and someone else figures "And also it'd be much easier to write up a control circuit that always expects three digits" and eventually everyone is confused if we're looking at the user input as a stream of tuples of three digits, instead of looking at the last three digits in a stream of digits. It was a very instructive class.