About Theory projects in Part II [01BF]
Although the vast majority of Part II students seem to undertake projects in machine learning, a growing number of students wish to do a project in Theory, often specifically programming languages and semantics. This is definitely possible to do, but after marking dozens of Part II projects in all areas, I have seen that the PL projects tend to be of lower quality on the scales that are assessed for Part II than ones in other areas, so I would like to accumulate here some advice for students considering Theory.
The first thing to keep in mind is that a Part II project is required to have a significant engineering artefact associated with it. This is because we are actually assessing your readiness to work as a professional in the area of computing. Naturally, the specific nature of this artefact differs by the kind of project.
- In some projects, the artefact takes the form of a well-engineered computer system. For example, a compiler or a distributed system or a video game engine or something.
- In a data science project, the artefact might look a bit different because the goal is not to create a reusable computer system but instead to process specific data. The requirements for the “engineering” of a project like this are obviously different from those expected of a normal codebase, but nonetheless we require something significant and original and carefully designed to be happening here.
- In many Theory-adjacent projects, students may formalise some mathematics in a proof assistant like Isabelle, Agda, Rocq, or Lean.
In all cases, it is a requirement that the engineering output be significant, and the kind of thing that involves some deliberate design. We are not directly evaluating you on the basis of how many lines of code you write, but an artefact that has only a few hundred lines of code (or less) is almost certainly not going to be deep enough to meet the requirements of a Part II project.
It has been debated as to whether Theory projects should be judged differently. The main point for you to know is that as of right now, they are not judged differently. We do not currently set a lower bar for Theory projects, and I do not favour doing so in the future. If you choose to formalise some results in a proof assistant, the nature of the code is obviously different from (e.g.) writing a compiler or a video game engine, but given that some of your fellow students will actually be writing compilers and video game engines, consider whether the (Agda, Rocq, Lean, etc.) code you have written is comparably deep and difficult.