# A 2024 Computer Science Curriculum

## Table of Contents

## What is this

This is a dive into what Robert Harper calls computational trinitarianism where the theory of computation manifests itself in three forms: Logic, Languages and Categories. Any route can get you to the 'divine notion of computation'.

We only have access to nice things old exams, labs, and assignments if you don't pester the schools/profs as it's a breach of academic conduct for them to comment on any assignments to outsiders. If you want to meet the leading researchers visit a Topos Insitute seminar or pay for industry registration to the next OPLSS, POPL or HoTT workshop that is how you get involved. If you want to learn this material with a community some have started a Discord channel.

## Intros

### How to write a proof

This is a benefit of dependently typed languages your future 'discrete math' intro course that every undergrad teaches can all be done with a proof assistant now.

*The Mechanics of Proof*using Lean by Heather MacBeth

### Intro to Programming

- 15-150 Principles of Functional Programming (SML)
- Older Assignments & labs can be grabbed from here and here
- TAs wrote helpful docs for 15-150
- We can also try whatever current version of hype for types

- Programming with Categories a workbook (Haskell)

They are going to fully mechanize 15-210 soon using calf/decalf to prove costs.

- 15-210 Parallel & Sequential Algorithms (SML)
- Some recitations/review videos here but we won't need them
- The hw/labs can be found here or here
- A very detailed rewrite of the regex matcher from Harper's SML book for proof directed debugging but now with efficient backtracking
- Functional Data Structures by Prof Ragde (OCaml)

## Computational Trinity

### Programming Languages

*Practical Foundations for Programming Languages*book and supplementary materials- Robert Harper OPLSS 2021 lectures and some earlier OPLSS lectures for his book
- We have access to older 15-312 assignments (SML)

- PLAI a workbook (Racket/Lisp)

The HoTT seminar explains how univalence works which will be needed to understand how equality works in many new type theories

- 15-819 Homotopy Type Theory and book
- Programming in MLTT book

### Logic

Whatever proof theory and categorical logic we can get our hands on

- Constructive Logic (SML)
- How to read/use The Edinburgh Logical Framework or LF
- technical details we have to know

- Logical relations and LR as types or ParamTT
- 80-514 Categorical Logic

### Categories

Mac Lane's or Emily Riehl's book is accessible too if we learn some insights into basic algebraic topology.

- MIT course Applied Category Theory
*Categories for Types*by Crole or Awodey's book

#### Applications

See the Topos Institute for more.

- Project that Robert Harper calls 'the greatest and most ignored idea' how they designed a network protocol stack in SML by combining two modules that share specs/cohere (a pullback)
- Network Programming OPLSS lectures provide a comprehensive intro to the theory and practice of network programming (OCaml)

#### Research

Robert Harper once spent an entire week reading the source of an operating system to find out in complete detail exactly what happened when he pushed a button on his keyboard how it ended up transformed as pixels on his screen. His advice to grad students is to develop a point of view so when you start a project articulate exactly why it's worthwhile and keep this perspective when you are deep into the seemingly impossible technical details.

## BEGIN

I'm going to start with the book *The Mechanics of Proof* because 15-150 will assume we know some of this as most CMU students will be taking 15-151 at the same time as 15-150.

- Workbook The Mechanics of Proof Fordham 2023
- See these install instructions
- There's many demos on YouTube by the author Heather Macbeth

#### Local install

Gitpod free tier is easiest. To install Lean locally w/Visual Studio:

- install Lean
- install git
- install code (Visual Studio code) though I use emacs see below
- in terminal type: git clone https://github.com/hrmacbeth/math2001.git
- cd math2001
- in terminal: lake exe cache get
- it downloads 3972+ files (wtf)

- 'code .' to start from present directory
- install lean4 extension

Click on 01ProofsbyCalculation.lean you should get a right panel opening up in VS code called 'Lean Infoview' that displays tactic state goals and all messages.

#### Emacs

Install everything as before then git clone lean4-mode, paste the readme elisp into .emacs or init.el file, restart and open any .lean file. Ctrl-c Ctrl-i opens the lean view in a new window showing goals. If you use vanilla emacs from some distros like Ubuntu you'll have some 'can't verify signature' error which is fixed by updating elpa keyring.

Another way is with gpg:

gpg --homedir ~/.emacs.d/elpa/gnupg --list-keys /home/x/.emacs.d/elpa/gnupg/pubring.kbx ----------------------------------------- pub dsa2048 2014-09-24 [SC] [expired: 2019-09-23] CA442C00F91774F17F59D9B0474F05837FBDEF9B uid [ expired] GNU ELPA Signing Agent (2014) <elpasign@elpa.gnu.org> pub rsa3072 2019-04-23 [SC] [expires: 2024-04-21] C433554766D3DDC64221BFAA066DAFCB81E42C40 uid [ unknown] GNU ELPA Signing Agent (2019) <elpasign@elpa.gnu.org> pub ed25519 2022-12-28 [C] [expires: 2032-12-25] AC49B8A5FDED6931F40EE78BF993C03786DE7ECA uid [ unknown] GNU ELPA Signing Agent (2023) <elpasign@elpa.gnu.org> sub ed25519 2022-12-28 [S] [expires: 2027-12-27]

Update key if your second key is expired:

gpg --homedir ~/.emacs.d/elpa/gnupg --keyserver hkps://keys.openpgp.org --recv-keys 066DAFCB81E42C40

### Proving equalities

Reading 1.1 *Proving equalities* from Mechanics of Proof. Any examples you don't understand come back here after writing some Lean proofs you won't get them all immediately. First example expand out (a - b) and notice you need to add 4ab in order to balance both sides. The problem statement tells us (a - b) = 4 so (a - b)^{2} is 16 after substitution.

1.2.x *Proving equalities in Lean* the .lean files are all included in the Math2001 directory you cloned from github. I had to fight with Lean to get it to accept 1.2.4 so rewrote it exactly like she did with parens:

-- Example 1.2.4. -- Exercise: type out the whole proof printed in the text as a Lean proof. example {a b c d e f : ℤ} (h1 : a * d = b * c) (h2 : c * f = d * e) : d * (a * f - b * e) = 0 := calc d * (a * f - b * e) = d * a * f - d * b * e := by ring _ = (a * d) * f - d * b * e := by ring _ = (b * c) * f - d * b * e := by rw [h1] _ = b * (c * f) - d * b * e := by ring _ = b * (d * e) - d * b * e := by rw [h2] _ = 0 := by ring

We are using 'calc' in Lean hence the name proof by calculation. I'm guessing the underscore represents the entire left hand side of the equation indicating to the rw (rewrite) pattern matcher to ignore it. There's nothing in the documentation I could easily find but Terence Tao describes the underscore here same way.

Look at the infoview/goals it will tell you when that stage is done by 'goals accomplished', also click around various parts of the proof to see how the infoview changes:

-- Example 1.3.2 example {x : ℤ} (h1 : x + 4 = 2) : x = -2 := calc x = (x + 4) - 4 := by ring _ = 2 - 4 := by rw [h1] _ = -2 := by ring

I guessed the syntax for rationals in Lean and it worked:

-- Example 1.3.4 example {w : ℚ} (h1 : 3 * w + 1 = 4) : w = 1 := calc w = (3 * w + 1)/3 - 1/3 := by ring _ = 4/3 - 1/3 := by rw [h1] _ = 1 := by ring

1.3.11 you can use Lean to tell you when the sides have been balanced. You did it correctly if goals panel or infoview shows goals accomplished and the linter hasn't added any red squiggle lines or other errors. Some exercises I tried, you can rewrite a line using both hypotheses and eliminate a lot of steps I kept them here for illustration how Lean works:

example {u v : ℚ} (h1 : 4 * u + v = 3) (h2 : v = 2) : u = 1 / 4 := calc u = (4 * u + v)/4 - v/4 := by ring _ = 3/4 - 2/4 := by rw [h1, h2] _ = 1/4 := by ring example {u v : ℝ} (h1 : u + 1 = v) : u ^ 2 + 3 * u + 1 = v ^ 2 + v - 1 := calc u ^ 2 + 3 * u + 1 = (u + 1) * (u + 1) + (u + 1) - 1 := by ring _ = v * v + v - 1 := by rw [h1] _ = v ^ 2 + v - 1 := by ring

### Tips and tricks

1.3.2 once again we first establish x = x then use the hypothesis to rewrite it

-- Example 1.3.2 example {x : ℤ} (h1 : x + 4 = 2) : x = -2 := calc x = (x + 4) - 4 := by ring _ = 2 - 4 := by rw [h1] _ = -2 := by ring

For the rest of these examples try them yourself going through the 03TipsandTricks.lean file before looking at the solution it's the only way you learn.

-- Example 1.3.5 example {x : ℤ} (h1 : 2 * x + 3 = x) : x = -3 := calc x = (2 * x) - x := by ring _ = 2 * x - (2 * x + 3) := by rw [h1] _ = -3 := by ring

(╯°□°)╯︵ ┻━┻ if you see calc underlined with a red error it means you forgot an equal sign or _ sign in your chain of rewrites or there is an accidental character floating around in the scope out of view somewhere it took me forever to figure that out as Lean kept giving some cryptic message and I was looking at the signature.

1.3.11 exercises all use the examples we just saw. Look at 1.3.8 example when you try exercise 11 and manipulate it so a = (4 + 2) / 3.

example {x y : ℝ} (h1 : x = 3) (h2 : y = 4 * x - 3) : y = 9 := calc y = y := by ring _ = 4*x - 3 := by rw [h2] _ = 4*3 - 3 := by rw [h1] _ = 9 := by ring example {p : ℝ} (h1 : 5 * p - 3 = 3 * p + 1) : p = 2 := calc p = (5*p -3 - 3*p + 1)/2 + 1 := by ring _ = (3*p + 1 - 3*p + 1)/2 + 1 := by rw [h1] _ = 2/2 + 1 := by ring _ = 2 := by ring

### Proving inequalities

We're still doing the proofs by calc chapter.

1.4.1 example copy down some of the general rules

- Inequality preserved if C \(\ge\) 0:
- A \(\ge\) B implies CA \(\ge\) CB
- A \(\ge\) B implies A - C \(\ge\) B - C
- A \(\ge\) B and B > C then A > C

- Reversed inequality:
- A \(\ge\) B implies C - B \(\ge\) C - A
- 2 \(\ge\) 1 implies 5 - 1 \(\ge\) 5 - 2

To get the full list of the unicode symbols every editor plugin comes with an abbreviations.json file. Place '\' (LaTeX style commands) before any of those symbols on the left of the abbreviations file to see them converted to the symbols on the right. For example \b is converted in the editor to \(\beta\)

\ge greater or equal \le less than or equal < and > are just unicode keyboard chars

-- Example 1.4.2 -- Exercise: replace the words "sorry" with the correct Lean justification. example {r s : ℚ} (h1 : s + 3 ≥ r) (h2 : s + r ≤ 3) : r ≤ 3 := calc r = (s + r + r - s) / 2 := by ring _ ≤ (3 + (s + 3) - s) / 2 := by rel [h1, h2] _ = 3 := by ring

Example 1.4.3 think why is x + y <= x + (x + 5) it's because y <= x + 5 and x is <= to itself.

-- Example 1.4.3 -- Exercise: type out the whole proof printed in the text as a Lean proof. example {x y : ℝ} (h1 : y ≤ x + 5) (h2 : x ≤ -2) : x + y < 2 := calc x + y ≤ x + (x + 5) := by rel [h1] _ = 2 * x + 5 := by ring _ ≤ 2 * -2 + 5 := by rel [h2] _ < 2 := by numbers

Example 1.4.6 the final tactic is := by extra which is defined if you click on 'Index of Lean tactics' as "extra checks an inequality whose two sides differ by the addition of a positive quantity".

-- Example 1.4.9 -- Exercise: replace the words "sorry" with the correct Lean justification. example {a b : ℚ} (h1 : a ≥ 0) (h2 : b ≥ 0) (h3 : a + b ≤ 8) : 3 * a * b + a ≤ 7 * b + 72 := calc 3 * a * b + a ≤ 2 * b ^ 2 + a ^ 2 + (3 * a * b + a) := by extra _ = 2 * ((a + b) * b) + (a + b) * a + a := by ring _ ≤ 2 * (8 * b) + 8 * a + a := by rel [h3] _ = 7 * b + 9 * (a + b) := by ring _ ≤ 7 * b + 9 * 8 := by rel [h3] _ = 7 * b + 72 := by ring

1.4.10 same tactic used, put left hand side of inequality on right and side, add some positive squares. If you use any symbolic calculator online then the enormous expanded square makes sense as (a^{4} + b^{4} + c^{4})^{2} = a^{8}+2a^{4}b^{4}+2a^{4}c^{4}+b^{8}+2b^{4}c^{4}+c^{8}

Try some 14.11 exercises

example {a b : ℚ} (h1 : 3 ≤ a) (h2 : a + 2 * b ≥ 4) : a + b ≥ 3 := calc a + b = a/2 + (a + 2*b)/2 := by ring _ ≥ 3/2 + 4/2 := by rel [h1,h2] _ ≥ 3 := by numbers example {x : ℤ} (hx : x ≥ 9) : x ^ 3 - 8 * x ^ 2 + 2 * x ≥ 3 := calc x ^ 3 - 8 * x ^ 2 + 2 * x = x * x * x - 8 * x * x + 2 * x := by ring _ ≥ 9 * x * x - 8 * x * x + 2 * x := by rel [hx] _ = x * x + 2 * x := by ring _ ≥ 9 * x + 2 * x := by rel [hx] _ = 11 * x := by ring _ ≥ 11 * 9 := by rel [hx] _ ≥ 3 := by numbers example {n : ℤ} (hn : n ≥ 10) : n ^ 4 - 2 * n ^ 2 > 3 * n ^ 3 := calc n^4 - 2 * n^2 = n * n^3 - 2 * n^2 := by ring _ ≥ 10 * n^3 - 2 * n^2 := by rel [hn] _ = 3 * n^3 + 7 * n * n * n - 2 * n * n := by ring _ ≥ 3 * n^3 + 7 * 10 * n * n - 2 * n * n := by rel [hn] _ = 3 * n^3 + 68 * n * n := by ring _ ≥ 3 * n^3 + 68 * 10 * 10 := by rel [hn] _ > 3 * n^3 := by extra

Exercise 6 I couldn't figure it out in lean as I don't know enough of the standard library yet as there's no hypothesis to use rel or addarith with and the sig wants a rational number. My attempts using squares with the tactic extra failed too whereas by hand it is easy:

- x
^{2}- 2x \(\ge\) -1 - x
^{2}- 2x + 1 \(\ge\) -1 + 1 - (x - 1)
^{2}\(\ge\) 0- which we know is true since squares are always positive

### Proofs with structure

Reading the second chapter.

2.1.2 prove m + 3 = 9 then final tactic is addarith to subtract 3 from both sides and show m = 9 - 3 or 6.

2.1.5 example remember extra checks an inequality whose two sides differ by the addition of a positive quantity and the square b^{2} is always positive.

Another example is 2.1.7 of extra since positive quantities

example (a b : ℝ) (h1 : -b ≤ a) (h2 : a ≤ b) : a ^ 2 ≤ b ^ 2 := by have h3 : 0 ≤ b + a := by addarith [h1] have h4 : 0 ≤ b - a := by addarith [h2] calc a^2 ≤ a^2 + (b + a) * (b - a) := by extra _ = b^2 := by ring

2.1.8 extra tactic again:

example (a b : ℝ) (h : a ≤ b) : a ^ 3 ≤ b ^ 3 := by have h2 : 0 ≤ b - a := by addarith [h] calc a^3 ≤ a^3 + ((b-a)*((b-a)^2 + 3*(b + a)^2)/4) := by extra _ = b^3 := by ring

The cancel tactic is defined as follows if you look at the code it's another tactic written for this book to simplify the regular lean libraries which are all abstract algebra we haven't learned yet.

'Cancel 2 at h' means

- 2x = 2y cancel to x = y
- 2x < 2y cancel to x < y
- x
^{2}= y^{2}cancel to x = y - 0 < 2x cancel to 0 < x
- x
^{2}= 0 cancel to x = 0

However in the exercises I couldn't get it work.

Example Ex 2.1.9 this is what I want to do but it won't let me despite x already being x > 1 so no possible way (x + 2) could be (-2 + 2) or 0:

example {x : ℚ} (h1 : x ^ 2 = 4) (h2 : 1 < x) : x = 2 := by have h3 := calc x * (x + 2) = 2 * (x ^ 2 + 2 * x)/2 := by ring _ = 2 * (4 + 2 * x)/2 := by rw [h1] _ = 2 * (x + 2) := by ring cancel (x + 2) at h3

Another example from 2.1.9 that doesn't work, I tried after to manually add in (h : n > 0) and still fails:

example {n : ℤ} (hn : n ^ 2 + 4 = 4 * n) : n = 2 := by have hm : 0 = n ^ 2 - 4 * n + 4 := by addarith [hn] have h1 := calc 0 = n ^ 2 - 4 * n + 4 := by rw [hm] _ = (n - 2)^2 := by ring cancel 2 at h1 addarith [h1]

Others have had problems too and filed an issue for a possible bug or maybe I don't understand how Lean4 tactics work we'll have to skip these and try them again later when the author replies.

### Invoking lemmas

TODO

## Principles of Functional Programming

There's no programming prereqs. 15-150 was designed so students who already had some background in high school CS or who took 15-122 *Principles of Imperative Computation* wouldn't have any kind of advantage. If they didn't have high school CS they would likely take 15-110/112 which is now some kind of CS academy but those legacy courses aren't needed.

### Lecture 1

Watching the first lecture. According to Robert Harper and Shriram Krishnamurthi so-called 'programming paradigms' like imperative, object-oriented or functional are vague descriptors of the same thing which is just programming. We'll work through both their books PFPL and PLAI after this course. The professor he talks about ~45m we're doing his constructive logic course after this too. @51m LaTeX is how you generate symbols like \(\implies\) for books/papers. Don Knuth invented the original program TeX (annoyingly pronounced 'tek') to write TAOCP.

If you want to follow what he's doing in the REPL try SOSML the online interpreter. The type annotations are optional in SML you can enter 'fun double n = n + n' though I would always use them in the beginning just to remember what you're doing.

#### PSML

Go to Robert Harper's CMU page and get Programming in Standard ML. Skip the overview (we'll do that regex debugging later) and start at Chapter 2 *Types, Values, and Effects*. In 2.1 if you don't remember what a polynomial is: f(x) = x^{2} + x^{1} + .. you bind x to an input value like x=1 then evaluate by rules of arithmetic the value of the polynomial at that given input f(1) = 1^{2} + 1^{1} + …

Harper is purposely provocative in all his writings and talks to get the reader/listener engaged and here he is claiming that the evaluation model of SML completely subsumes all other models where in only special cases would you program via execution of commands that manipulate memory and SML allows you to do both if needed. TODO

… cont