This paper gives the proof of a useful and non-trivial program, Quicksort (Hoare, 1961). First the general algorithm is described informally; next a rigorous but informal proof of correctness of the coded program is given; finally some formal methods are introduced. Conclusions are drawn on the possibility of enlisting mechanical aid in the proof process.