Presburger arithmetic is the first-order theory of the natural numbers with addition and order. This theory was shown decidable by M. Presburger in 1929. In the 1960s, Presburger arithmetic was studied in the context of formal language theory. Two of the main results from this period are that the sets of natural numbers definable in Presburger arithmetic are the so-called semi-linear sets, and that Parikh images of languages generated by context-free grammars are semi-linear and hence Presburger-definable. Subsequently, from the 1970s onwards the computational complexity of Presburger arithmetic received interest. The landmark results from this period are a doubly exponential lower bound shown by Fischer and Rabin in 1974 and a triply-exponential upper bound shown by Oppen in 1978. The 1980ies brought a more fine-grained complexity analysis of (fragments of) Presburger arithmetic by Fürer, Grädel and Scarpellini. In this talk, I will survey those classical results and show the relevant proofs or proof ideas for most of them. I will in depth discuss a recent result that shows that Presburger arithmetic with a fixed number of quantifier alternations is complete for every level of the weak EXP hierarchy. If time permits, I will discuss some recent work in which Presburger arithmetic has been used for showing new lower bounds for equivalence problems for commutative grammars.