This talk serves as an introduction to finite model theory -- an area of mathematical logic. Currently, finite model theory is used in theoretical computer science to study the logical foundations of computational complexity. This is done in the hope of understanding resource bounded computation from a machine independent point of view. The ordinary way to solve a problem in computer science is to demonstrate an algorithm which will run on an appropriate machine model of computation. In fact, computer science is often succinctly defined as the study of algorithms. We shall explain descriptive complexity -- the notion of solving a problem by simply expressing its solution as a formula in some logic. This turns out to be a more natural approach from the mathematical point of view, as it does not involve converting the natural domain of discourse (say graphs) into bits of a binary string to be processed by the instruction set of a particular machine. The main interest and excitement is in the close connection between this approach of expressing a solution (with a formula in some logic) to the more classical approach of providing an algorithm (with a program to run on some machine). In particular, relating cyclic first-order formulas in logic to polynomial time bounds on machines, we are left with a tantalizing question: Is there an effective enumeration of all the polynomial time computable properties of graphs? We illustrate how the answer to this and other related questions has a direct bearing on P vs. NP -- the most famous unresolved problem in theoretical computer science.