The Life and Loves of Academic Writing

You may not experience love at first sight with many academic texts. Do you sometimes find them overdressed, distant, or complicated? Understanding why something is the way it is can help us appreciate it and maybe even gain intimacy. Therefore, let’s look at two texts on the same topic in order to discern some key traits of academic writing in English: the transcription of a clip from an academic lecture and an excerpt of an academic article. When we speak, we often have different priorities than when we write. By looking at the differences between how similar information is expressed in a lecture versus an academic article, we can deduce some commonly accepted conventions of academic writing.

Both texts are presented by one of my favorite academics, Philip Wadler, who is a professor of theoretical computer science at the University of Edinburgh.

I have transcribed the first five minutes of one of Wadler’s lectures. I highly recommend watching the first few minutes of the lecture first, or at least listening along to Wadler in the video while reading. As you read the talk transcript, try to identify elements that you would not expect to find in an academic article. You might pretend you are the editor of an academic journal and begin taking note of the changes you would suggest in order to transform the talk text into a journal article.

“Propositions as Types,” by Philip Wadler

Transcript of the first five minutes of the lecture, “Propositions as Types,” by Philip Wadler

“Are you ready to learn about the hilarious subject of computability theory? An algorithm is a sequence of instructions followed by a computer. Now you all think of computers as machines, but for an awful long time what a computer meant was a person: the person who executed the algorithm. Algorithms go back to Euclid’s Elements in classical Greece and to eponymously Al-Khwarizmi in 9th century Persia. But a formal mathematical definition doesn’t appear until the 20th century, when you have proposals by Alonzo Church, Curt Gödel, and Alan Turing, all appearing within a year of each other. It’s like buses. You wait 2000 years for a definition of effective computability and then three come along at once. Why did this happen?

So, at the dawn of the 20th century, one of the foremost proponents of formal logic was David Hilbert in Göttingen. And what he wanted to do was put all mathematicians out of business. What he wanted was an algorithm that, given a statement in formal logic, would determine if that statement was true or false. This was called the Entscheidungsproblem because it sounds a lot better in German. It just means decision problem. And what Hilbert was depending upon was the idea that logic is complete, meaning every provable statement is true, and every true statement is provable. Sound reasonable, right? Except in 1930 in Vienna, Curt Gödel published his proof of the incompleteness theorem, and this meant that Hilbert was, to use a technical term, screwed.

So, what Gödel showed was that any logic powerful enough to represent arithmetic could encode the following statement: this statement is not provable. The way he did this is he used a clever technique called Gödel Numbering to encode statements and proofs as numbers, which is why he depended upon arithmetic. So, don’t worry about the details about how he did that, although it is one of the world’s first functional programs. But think about this statement: this statement is not provable. Boy. Right? As soon as you have this statement written down, you are in trouble. Why? Right, so it’s very much like what we heard with the liar’s paradox, only now it’s provability. So what happens? Well, if it’s false, then it is provable, and you’ve proved something that’s false. This is really bad news. You don’t want to do that. So, the alternative is that it’s true, but now you must have a statement that is true but not provable. So, that’s not as bad, but it’s still really annoying, especially if you’re Hilbert.

Now, as long as people thought there’d be a solution to the Entscheidungsproblem, you didn’t need a formal definition of algorithm. You just write down the algorithm that was the solution, and it would be like Justice Potter’s definition of pornography: I know it when I see it. But if your goal is to show the Entschiedungsproblem is undecidable, then you need a formal definition of algorithm, so you can show that no algorithm is going to work. So, the race was on.

The first solution was proposed by Alonzo Church in Princeton. He came up with this thing called Lambda Calculus in 1932 and by 1936, he’d used to to show that, yes, if an algorithm is what you can express in Lambda Calculus, then it’s the case that Entscheidungsproblem is undecidable. He actually did this by means of something else that was undecidable, which we now call the halting problem.”

Once you have had a chance to note some elements that might need to be altered before publishing the above text in an academic journal, let’s look at a portion of similar content that was actually published in an academic article. Again, let’s take note of some of the major differences between the two texts.

Excerpt from “Propositions as Types,” by Philip Wadler


“As the 20th century dawned, Whitehead and Russell’s Principia Mathematica demonstrated formal logic could express a large part of mathematics. Inspired by this vision, Hilbert and his colleagues at Göttingen became the leading proponents of formal logic, aiming to put it on a firm foundation.

One goal of Hilbert’s Program was to solve the Entscheidungsproblem (decision problem), that is, to develop an “effectively calculable” procedure to determine the truth or falsity of any statement. The problem presupposes completeness—that for any statement, either it or its negation possesses a proof. In his address to the 1930 Mathematical Congress in Königsberg, Hilbert affirmed his belief in this principle, concluding “Wir müssen wissen, wir werden wissen” (“We must know, we will know”), words later engraved on his tombstone. Perhaps a tombstone is an appropriate place for these words, given that any basis for Hilbert’s optimism had been undermined the day before, when at the selfsame conference Gödel18 announced his proof that arithmetic is incomplete.

While the goal was to satisfy Hilbert’s program, no precise definition of “effectively calculable” was required. It would be clear whether a given procedure was effective or not, like Justice Stewart’s characterization of obscenity, “I know it when I see it.” But to show the Entscheidungsproblem undecidable required a formal definition of “effectively calculable.”

One can find allusions to the concept of algorithm in the work of Euclid and, eponymously, al-Khwarizmi, but the concept was formalized only in the 20th century, and then simultaneously received three independent definitions by logicians. Like buses, you wait 2,000 years for a definition of “effectively calculable,” and then three come along at once. The three were lambda calculus, published in 1936 by Church,7 recursive functions, proposed by Gödel at lectures in Princeton in 1934 and published in 1936 by Kleene,24 and Turing machines, published in 1937 by Turing.36

Lambda calculus was introduced by Church at Princeton, and further developed by his students Rosser and Kleene. At that time, Princeton rivaled Göttingen as a center for the study of logic. The Institute for Advanced Study was co-located with the Mathematics Department in Fine Hall. In 1933, Einstein and von Neumann joined the Institute, and Gödel arrived for a visit.

18.  Gödel, K. Über formal unterscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatshefte für Mathematik und Physik 38 (1931), 173–198; reprinted in Heijenoort.37

37.  van Heijenoort, J. From Frege to Gödel: A Sourcebook in Mathematical Logic, 1879–1931. Harvard University Press, Cambridge, MA, 1967.

7.   Church, A. An unsolvable problem of elementary number theory. American Journal of Mathematics 58, 2 (Apr. 1936), 345–363; presented to the American Mathematical Society, Apr. 19, 1935; abstract in Bulletin of the American Mathematical Society 41 (May 1935).

24.  Kleene, S.C. General recursive functions of natural numbers. Mathematical Annalen 112, 1 (Dec. 1936); abstract in Bulletin of the AMS (July 1935).

36.  Turing, A.M. On computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society s2–42, 1 (1937); received May 28, 1936, read Nov. 12, 1936.

Wadler, Philip. “Propositions as Types.” Communications of the ACM, Association for Computing Machinerey, 1 Nov. 2015,

How many of the following characteristics did you identify in the academic article version of the “Propositions as Types” text?

What are some of the main differences between the two texts?

By comparing the two texts of Professor Wadler above, let’s tease out some priorities of academic writing.

  1. Which text is shorter?
  2. Which text avoids contractions and spells words out in their complete form, such as “it is,” instead of “it’s”?
  3. Which text maintains more objective distance by focusing on the content rather than drawing frequent attention to the author, “I,” and the audience, “you”?
  4. Which text includes citations and a references list to indicate where information comes from?
  5. Which text uses more formal diction, avoiding informal or imprecise words and phrases like “screwed,” “bad,” and “a lot”?
  6. Which text includes a richer set of transitions and other sentence starters, rarely beginning sentences with “But,” “And,” “So,” and “Well”?
  7. What other differences between the two texts strike you?
  8. Does anything surprise you about either text?

Successful scholars often have the opportunity to break some of the “rules” that others of use are required to follow. Which conventions of academic writing would you say are non-negotiable?

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s