Lecture 1: Intro
1 Purpose
Introduce the class, give high-level motivations.
2 Outline
This course: newly redesigned, taking lessons from what worked and didn’t work about the course in the past, but also, from the world around us (program synthesis). While program synthesis is an incredibly old field, it was never something that seemed remotely mainstream until the last year or two. We have no way of predicting the programming languages, frameworks, tools, etc that you’ll be using when you graduate, but it seems pretty likely at this point that AI-based program synthesis will be involved.
Why does this matter, and what does this have to do with this course? While program synthesis tools are already pretty good at going from prompts to code, and will only get better, they will always be vulnerable to producing things that, even if they look plausible, simply aren’t right. Or have security vulnerabilities. The output thus needs to be checked, and the best way to check it is to have a precise description of what the code should do: a specification. Armed with a specification, synthesis can be turned loose, as only synthesized programs that satisfy the spec will be accepted.
So what we want to do with this course is both teach you what specifications are and how to write them and show you how specifications can be connected to programs. While we believe the former skills will become mainstream over the next decade or so, the latter will position you to be able to help build the tools that take synthesis mainstream. Certainly, working on the models themselves requires other skills: modern AI techniques involving deep learning, neural networks, etc. but we’re not concerned with that: these models exist and will continue to get better. If you’re interested in that, certainly take courses on those topics! In this class, what we’re interested in is how to connect the models to reality, and that’s where specifications come in. We’ll use a variety of techniques in this class, and there are many more that we won’t cover, but having learned this, you’ll be in a position well ahead of those who haven’t had this background.
So let’s get started.
What is logic?
What is computation?
Are these things connected?
Goal of this class: Learn how to write down precise descriptions of what code should do, and to discover how these properties can relate to the programs you are building.
Problem with descriptions: imprecision. One of most valuable domains: medical devices. Consider designing an automatic insulin pump. It has electronics that periodically measure blood sugar, and separately can deliver insulin to correct when blood sugar goes too high. Having too little insulin in people with Type 1 diabetes is obviously a problem: hence the insulin pump, but delivering too much insulin is also bad. Clearly, the software that reads the measurements and decides how much insulin to deliver is quite important. How do we ensure it does the right thing?
First, we need to have a precise way of describing its behavior. You can try to do this in English, and likely, will start that way, but English has all sorts of ambiguities: take the word "or". In English, it usually means exclusive or, but sometimes might mean non-exclusive or. In cases where a little ambiguity is fine (or indeed, desired: literature would be quite boring if not for this!), this is fine, but when it comes to places where we want the exact behavior to be understood and checked (by doctors and scientists, in the case of the insulin pump), that’s not great.
So instead, we turn to more formal languages. In this, logic is a great asset, as it allows us to give precise meaning to what we want.
How would we begin to describe how an insulin pump should work? One key idea, especially when describing systems that operate over time, is to describe certain temporal properties that it should have. For example, there might be some dosage that should never be exceeded over a certain time interval, no matter what else the system was doing. Consider that the main control function for the pump took two arguments: a history of blood sugar readings, and a history of insulin doses (each, say, every second), and we need to determine what dosage to give at the next second (which, next time our control function is called, will be the entry at 0 SecondsAgo). We could represent each of those as function types, so the type of our control function might be:
; control : [SecondsAgo -> BloodSugar] [SecondsAgo -> InsulinGiven] -> InsulinGiven
If we wanted to never exceed a certain total dosage, say MAX-DOSE-OVER-T, over a certain interval T, we could express that logically with the statement:
\forall (Hx : SecondsAgo \rightarrow BloodSugar) (Rx : SecondsAgo \rightarrow InsulinGiven).\\ \quad \sum_{i=1}^{T} Rx(i) \lt \text{MAX-DOSE-OVER-T} \implies \\ \quad control(Hx, Rx) \lt \text{MAX-DOSE-OVER-T} - \sum_{i=1}^{T} Rx(i)
There might be simpler properties we also want to hold: never giving more than MAX-DOSE at a single time, regardless of the readings or history of dosages:
\forall (Hx : SecondsAgo \rightarrow BloodSugar) (Rx : SecondsAgo \rightarrow InsulinGiven).\\ \quad control(Hx,Rx) \lt \text{MAX-DOSE}
And then, of course, once we get past the safety requirements, we can start expressing properties about what we should give in terms of dosing: clearly, these requirements need to come from experts, but they can then be expressed in terms of properties that use the history of readings & history of dosings. Let’s say we wanted to express that if the blood sugar reading average was above 200 over the past 120 readings, and less than 10 units of insulin given (intentionally not giving units, to not give innacurate medical information), deliver 1 unit.
\forall (Hx : SecondsAgo \rightarrow BloodSugar) (Rx : SecondsAgo \rightarrow InsulinGiven).\\ \quad ((\sum_{i=1}^{120} Hx(i)/120) \ge 200) \land ((\sum_{i=1}^{120} Rx(i)) \lt 10) \implies \\ \quad control(Hx, Rx) = 1
All of these have used a logical operator from first-order logic: for-all. We use this to express that these are properties that should hold no matter what values come in.
This course is about writing specifications. We want to connect the logical operators that you learned about in Discrete with actual code, as seen above. But it is also about learning how to use those specifications. We will deploy a variety of tools, so by the end, you’ll understand quite a bit of the landscape. What underlies all of them are logical properties, but the tools are quite different.
For the first few weeks, we’ll use a language called isl-spec, which extends the Intermediate Student Language from CS2500 with support for property-based testing. We’ll learn how to formulate logical properties as code, and how to use PBT to partially check those properties. You can install it from within DrRacket (need version 8.6 or 8.7) by going to File -> Install Package..., and then searching for isl-spec.
We’ll learn that the representation of properties also matters. While the function (map) representation above might seem natural, functions are somewhat opaque, and we might have an easier time reasoning about a sequence of readings. We can make that change, and then actually run some of our properties.
For example, consider a prototype (and wrong) implementation of the above control function. We’ve changed the representation of our histories to lists instead of functions, as with the property-based testing tooling, the primary goal is to find counter-examples, and lists will print out, whereas functions are opaque. The question of data representation in order to support reasoning is an important one, and one that we’ll return to.
#lang isl-spec
; get-n-readings : [List-of Natural] Natural -> [List-of Natural]
(define (get-n-readings l n)
(cond [(empty? l) (cond [(zero? n) '()]
[(positive? n) (build-list n (λ(_) 0))])]
[(cons? l) (cond [(zero? n) '()]
[(positive? n) (cons (first l)
(get-n-readings (rest l)
(sub1 n)))])]))
; sum : [List-of Number] -> Number
(define (sum lon) (foldr + 0 lon))
; average : [List-of Number] -> Number
(define (average lon) (/ (sum lon) (length lon)))
; control : [ListOf BloodSugar] [ListOf InsulinGiven] -> InsulinGiven
; takes history of readings, history of dosing (any further back unknown), calculates new dose
(define (control Hx Rx)
1)
(define MAX-DOSE-OVER-T 10)
(define T 60)
(define MAX-DOSE 2)
(check-property (for-all [(Hx [ListOf Natural]) (Rx [ListOf Natural])]
(let [(already-given (sum (get-n-readings Rx (- T 1))))]
(==> (< already-given MAX-DOSE-OVER-T)
(< (control Hx Rx) (- MAX-DOSE-OVER-T already-given))))))
(check-property (for-all [(Hx [ListOf Natural]) (Rx [ListOf Natural])]
(< (control Hx Rx) MAX-DOSE)))
We’ll next learn to use a tool called Rosette, with leverages an SMT solver under the hood to do much more exhaustive checking of a restricted subset of properties. SMT solvers generalize solvers for the SAT problem in boolean propositional logic to other theories, including ones that involve numbers, bitvectors, strings, etc. They are carefully limited in expressivity to allow surprisingly effective solvers, especially given even plain-old SAT is exponential in the naive case: you have to check all of the possible assignments. SMT solvers are an incredibly important topic, and used extensively in industry. We’ll only spend a little bit of time on them, but enough to give you a sense of what they can do.
For the bulk of the semester, we’ll learn to use the theorem prover Lean. Lean is an industrial strength tool for expressing incredibly rich properties and writing code that satisfies those properties. The properties we can express are richer, and the level of trust that we get higher, but there’s a tradeoff: carrying out the proofs (as they are proofs!) is much more difficult than using either PBT or SMT.
3 Administrative
We’ll cover most of the actual logistics next class, as I wanted to have the first class be a bit more substantive, but a few important details:
1. Homework for this class can be done in groups of any size or individually, and you are welcome to get help from anyone on any homework: you just need to attribute those you got help from. When you submit your homework, you can submit in groups of any size: this has no impact on your grading, and if you work together, is much appreciated by the course staff, so we aren’t needlessly grading the same solution multiple times.
2. There will be in-class quizes nearly every day, which will be small but not trivial: as long as you are current with the material, you should be able to pass them. collectively, they count towards 40% of your grade, though we will drop about 1/3 of them to not punish missing some classes too severely.