Sipser's *Introduction to the Theory of Computation* spends some time motivating the need for precise definitions, since it's aimed towards a computer science audience who may not have experience with proofs. Here's what he has to say before the introduction of the first really formal definition in the book on page 35: <blockquote>In the preceding section we used state diagrams to introduce finite automata. Now we define finite automata formally. Although state diagrams are easier to grasp intuitively, we need the formal definition, too, for two specific reasons. <br><br> First, a formal definition is <b>precise</b> [emphasis added]. It resolves any uncertainties about what is allowed in a finite automaton. If you were uncertain about whether finite automata were allowed to have 0 accept states or whether they must have exactly one transition exiting every state for each possible input symbol, you could consult the formal definition and verify that the answer is yes in both cases. Second, a formal definition provides <b>notation</b> [emphasis added]. Good notation helps you think and express your thoughts clearly. <br><br> The language of a formal definition is somewhat arcane, having some similarity to the language of a legal document. Both need to be precise, and every detail must be spelled out.</blockquote> For a more mathematical example, you might want to spend some time talking about how hard it is to come up with a formal definition of polyhedron such that Euler's formula is actually true.