It was Max Dehn who said: "Solving the word problem for all groups may be as impossible as solving all mathematical problems." So when Boone and Novikov, working independently on opposite sides of the Iron Curtain in the 1950's, proved that there is a finitely presented group with unsolvable word problem, one had to start wondering what sorts of theorems might never be possible. Insolubility of the word problem is the basis for knowing that there are all sorts of things that cannot be solved or computed. And yet people continue to prove theorems. Dehn knew full well that even if you can't prove everything, there are still intelligent things to be said. He proved this by solving the word problem for fundamental groups of closed hyperbolic surfaces. In the 1980s, Gromov proved that the essential geometry of "Dehn's algorithm" can be applied to a vastly larger class of groups, now called word hyperbolic groups. At the same time, powerful algorithms and implementations have been developed and are playing substantive and essential roles in proving theorems. This talk will provide a quick survey of some of these developments.