Topos theory provides a dictionary between (certain areas of) logic and (certain areas of) geometry. As such, it provides all the benefits that mathematical dictionaries do: It lets you translate between two languages whose natural evolutions proceeded independently. An insight that is obvious in one domain may not be so obvious when translated to the other domain. Dictionaries cannot perform magic. In particular, it is usually too optimistic to think that a dictionary will allow you to prove significant new <i>theorems</i> with no effort. True, sometimes we do get lucky in this way. When Richard Stanley first discovered the dictionary between toric varieties and convex polytopes, he almost immediately reaped the reward of proving an important combinatorial conjecture with very little effort, because geometers had already put in a lot of work to solve exactly the problem he needed. But more commonly, the payoff of a dictionary is that it allows you to formulate good <i>questions</i> with very little effort. That is, you now have a new way to think about old problems, so you may be able to find your way more easily to a solution by borrowing concepts from both domains. You will still need to do hard work to solve hard problems, but your toolbox is now bigger.