Die theoretische Informatik beschäftigt sich mit der Theorie formaler Sprachen bzw. Automatentheorie, Berechenbarkeitstheorie, Komplexitätstheorie, Logik (u. a. Aussagenlogik und Prädikatenlogik), formaler Semantik und bietet Grundlagen für den Bau von Programmiersprachen und die Formalisierung von mathematischen Problemstellungen. Sie ist somit das formale Rückgrat der Informatik.

Sie beschäftigt sich außerdem mit der mathematischen Lösbarkeit von Problemen, also inwieweit sich Probleme überhaupt mathematisch formulieren und damit lösen lassen, und welchen Aufwand man dazu treiben muss.

Dabei werden formale Systeme, Automaten, Graphen und Syntaxdiagramme dazu genutzt, die innere Logik eines formalen Problems exakt wiederzugeben. Oft ist dieser formale Schritt ein wesentlicher Teil zur Lösung der eigentlichen Problemstellung und erschließt eine durch Maschinensemantik noch bequemer gewordene Welt der Mathematik und Computerei.