Welcome and Course Overview

\(\newcommand{\TirName}[1]{\text{#1}} \newcommand{\inferlab}[3]{ \let\and\qquad \begin{array}{l} \TirName{#1} \\ \displaystyle \frac{#2}{#3} \end{array} } \newcommand{\inferright}[3]{ \let\and\qquad \displaystyle \frac{#2}{#3}\TirName{#1} } \newcommand{\inferrule}[3][]{\inferlab{#1}{#2}{#3}} \newcommand{\infer}[3][]{\inferrule[#1]{#2}{#3}} \)

Puzzle

Suppose that you want to run some JavaScript programs—all the cool kids are doing it. However, you are deathy afraid that your mom/significant other/boss will see the curse word “BaNaNa” appear on you screen as the result of running the program. What do you do?

Safe?

1. Don’t run any programs. SAFE but USELESS.
2. Write a JavaScript interpreter that checks for “BaNaNa” before printing. SAFE but SLOW.

interpreter : Program x Data -> Data

Verifier

3. Write a verifier to make sure “BaNaNa” cannot printed and then run a fast interpreter if it passes the verifier.

verifier : Program -> Boolean

How do I write this verifier?

1. Always return false. SAFE but USELESS.
2. Fail if console.log appears (assuming all code). SAFE? No.
3. Fail if console.log(“BaNaNa”) appears. Definitely UNSAFE.

Soundness

Is our verifier sound?

Soundness is a property of a verifier that says if the program is safe, then the program is guaranteed to be safe. In this case, we want to guarantee that the program does not print “BaNaNa”.

Examples

var s = "BaNaNa"
console.log(s)

var f = console.log
f("BaNaNa")

var s = "B" + "a" + + "a" + "a"
console.log(s)

Course Oath

“I promise to support the learning of my fellow classmates, to not make any question feel unwelcome, to recognize our differing backgrounds, to the best of my ability.”