The radical development of formal methods in logic in the past two centuries has brought logic closer to mathematics, and, at the same time, accentuated the tension between the previously disparate fields. The driving foundationalist agenda, which attained dominance at the turn of the 20th century, is at tension with ordinary mathematical practice - as it threatens its autonomy by stripping it of ultimate authority as to what counts as valid proof.

In a recent book, Juliette Kennedy draws attention to this tension. The notion of formalism freeness has a central role in Kennedy's work, which, put concisely, means “the suppression of any […] aspects of a logic or formalism, except semantics”. In my talk I will pause on the distinction between formal and natural language that I take to be at the heart of the matter. Kennedy’s notion of formalism freeness that pertains to the subject matter of mathematical practice, but, arguably, it is first of all the freedom of the mathematician that it is at stake - the freedom to use their natural language. I then propose a reverse perspective by which formal language is where the freedom of the mathematician is most starkly exercised.