The introductory video included some background material on the software development process, i.e., the steps we go through from receiving a description of code to write and pushing it to end users. That material is background for all of the topics discussed below.
An introduction to writing code that runs in the browser. We will discuss the environment in which our code is run and the languages that we will use, JavaScript and TypeScript. We do not assume any prior knowledge of either language.
You may find that the second language you learn is actually the hardest! This can be because some things you took for granted in the first language are not the case in the second language. That can be unsettling, like the ground is shifting under your feet. In response, you feel like you need to look carefully at your feet as you take each step.... But that is exactly what we want for this course. We want to revisit core aspects of programming languages and make sure we have a complete understanding of how they work, what mistakes are possible and impossible. Having seen two languages, Java and TypeScript, will also help us understand the range of possibilities for what languages can do for us.
The introductory video noted that three principle techniques are used in practice to ensure that the programs we release to users are bug-free. These are testing, tools, and reasoning. In this topic, we will see that, while all three techniques are almost always needed, the amount of each needed depends on how complex the code is. We break this into level of difficulty based on the language features used.
We will, then, go into detail on the first two of those techniques: testing and tools. The remaining topics in the course will go into detail on the third and most important technique, reasoning.
Before we can apply correctness techniques at all, however, we must first know what the correct output should be, which is given to us by a specification. Since getting the details right is critical here, we will introduce a formal language to use for writing precise specifications.
In this topic, we begin learning about the most important tool for ensuring correctness: reasoning, which means thinking through what your code does to convince yourself that it is correct. Unlike testing, reasoning checks the correctness of all inputs, and unlike the type checker, reasoning ensures that the outputs are exactly what is required, not simply in the right set of values (the type).
Reasoning can be done formally or informally. Most professionals reason informally, in their heads. In class, we will learn formal reasoning because (1) it is much more teachable, (2) it contains key ideas needed for informal reasoning, and (3) it is required in practice for the hardest problems.
This week, we will start with the simplest case, which is reasoning about straight-line code without mutation. In the remaining topics, we will learn to reason about code that is not straight-line and then code that contains increasingly complex types of mutation.
This week, we continue to learn how to reason about code without mutation by moving on to code that involves recursion. Reasoning about recursion requires a new tool called structural induction. With that tool in hand, though, we have everything we need to handle any code that does not mutate.
With our set of reasoning tools now complete for non-mutating code, we turn our attention to other properties of high quality code: understability, changeability, and modularity. These properties are often provided by means of abstraction, which allows us to hide details of some parts of the code from other parts. This makes the code easier to understand and change, and allows multiple people to work on parts of the code simultaneously (modularity).
We will begin by studying how to hide the details of code via “procedural abstraction” and then see how to hide the details of data via “data abstraction”.
In this topic, we will finally begin to mutate local variables. Unfortunately, this substantially complicates reasoning about the code, requiring an entirely new set of tools called Floyd Logic. Fortunately, we will also see that there are additional tools, called forward and backward reasoning, that can mechnically translate complicated reasoning problems in Floyd Logic back into ones that our earlier tools are already capable of handling.
In this topic, we move to the next level of correctness difficulty, which involves mutating arrays. Once again, this new type of mutation will require additional tools. In this case, those are tools to keep track of facts about large parts of the array.
In this topic, we move to our highest level of correctness difficulty, which is when we allow heap state to be mutated. This allows us to perform some computations more efficiently, but at substantial cost, sometimes in the form of extaordinarily painful debugging. We will discuss ways to avoid that fate.
In this topic, we put together servers and stateful clients, forming “full stack” applications. Doing so, raises both the likelihood and costs of debugging. To keep the odds of debugging managable, we must apply rigorous type checking, testing, and reasoning of both the client and server individually. To succeed in debugging when it does occur, we must have a complete understanding of the client and server and how the two interact.
More topics as the course continues...