I agree that many objects in an OO approach suggest themselves, that would be of general use. "piles" that behave as stacks (push/pop) and show the top card or show no cards would be very common for all draw/discard piles. A "hand" of cards that presents the UI would also be good, but not needed for solitare. A deck would be derived from the stack and include shuffle and deal methods.

As for rules... that's the hard part. Writing code that uses these objects is straightforward. But describing it more formally so the objects simply interact the way they are required to? Might not be the way to go, since that's not how they operate in real life. The piles are not cogs in a clock or parts in a simulation; they are dumb data and an outside agent manipulates them and knows all the rules and plays.

However, I like the idea of putting in formal rules of play. This can be done with an expert system and backward-chaining logic. For example, you can only add a card to a pile if specific conditions are met, and this behaves as an exception if the play logic violates it. Then the rules of play are written in procedural logic, but can access the formal rules; e.g. obtain a list of legal discards before deciding which one to play. Then when it does discard (remove card from hand, push onto discard pile) it makes sure that this meets the formal criteria.