- Slides: 55
Download presentation
Computer Science at Carnegie Mellon Freshman IC Peter Lee Professor and Associate Dean
Envy
A Good Time to be Alive Your life My career
LIMITED WARRANTY. Microsoft warrants that (a) the SOFTWARE PRODUCT will perform substantially in accordance with the accompanying written materials for a period of ninety (90) days from the date of receipt, … LIMITATION OF LIABILITY. TO THE MAXIMUM EXTENT PERMITTED BY APPLICABLE LAW, IN NO EVENT SHALL MICROSOFT OR ITS SUPPLIERS BE LIABLE FOR ANY SPECIAL, INCIDENTAL, INDIRECT, OR CONSEQUENTIAL DAMAGES WHATSOEVER (INCLUDING, …) ARISING OUT OF THE USE OF … THE SOFTWARE PRODUCT… MICROSOFT’S ENTIRE LIABILITY … SHALL BE LIMITED TO THE GREATER OF THE AMOUNT ACTUALLY PAID BY YOU FOR THE SOFTWARE PRODUCT OR U. S. $5. 00; PROVIDED. . .
“If the automobile had followed the same development as the computer, a Rolls-Royce would today cost $100, get a million miles per gallon, and. . .
“If the automobile had followed the same development as the computer, a Rolls-Royce would today cost $100, get a million miles per gallon, and explode once a year killing everyone inside. " - Robert Cringely
Arianne 5
“Better, Faster, Cheaper”
The USS Yorktown “After a crew member mistakenly entered a zero into the data field of an application, the computer system proceeded to divide another quantity by that zero. The operation caused a buffer overflow, in which data leaked from a temporary storage space in memory, and the error eventually brought down the ship's propulsion system. The result: the Yorktown was dead in the water for more than two hours. ”
Some Advice
“Objects in calendar are closer than they appear”
Fail fast
“It was a dark and stormy night…”
Learn to express yourself in code
Hi!
Don’t be afraid of the faculty
Be a good team member and leader
“Students learn first and foremost from each other, and bringing them all together is the most important role of the university. ” — From “Quality Communication through Time and Space” James Morris, 1982
Think for yourself
History
Gates Center for Computer Science
Multimedia email MIME Andrew Message System Mulberry Cyrus …
Wired campuses And free internet access Established by CMU in 1982. . .
Java, Common Lisp Design projects started at CMU. . .
Who are you? >26 different states, >12 countries Median SAT near 1500 ~40 novice/beginner programmers ~33% women 96% predict graduating in the top half of the class The best students ever to walk the CMU campus.
Early curriculum Very intensive Attempts to give everyone a basic CS background in first two years Very open second two years Three different programming languages
“Programs must be written for people to read, and only incidentally for machines to execute. ” — Abelson and Sussman
“Programming is an explanatory activity. ” — Robert Harper
“If we spoke a different language, we would perceive a somewhat different world. ” — Wittgenstein
“C makes it easy to shoot yourself in the foot. C++ makes it harder, but when you do, it blows away your whole leg. ” —Bjarne Stroustrup
“The problem with using C++. . . is that there's already a strong tendency in the language to require you to know everything before you can do anything. ” — Larry Wall
“If you want a language that tries to lock up all the sharp objects and firemaking implements, use Pascal or Ada: the Nerf languages, harmless fun for children of all ages, and they won't mar the furniture. ” — Scott Fahlman
Be open-minded and have fun
“Once a logical formalism is established one can expect that a systematic, so-to-say computational, treatment of logic formulas is possible, which would somewhat correspond to theory of equations in algebra. ” — Hilbert, 1908
“I expect that digital computing machines will eventually stimulate considerable interest in symbolic logic… The language in which one communicates with these machines … forms a sort of symbolic logic. ” — Alan Turing
Formal Proofs Write “x is a proof of P” as x: P. Examples of predicates P: · (for all A, B) A and B B and A · (for all x, y, z) x<y and y<z x<z What do proofs look like?
Inference Rules We can write proofs by stitching together inference rules. An example inference rule: · If we have a proof x of P and a proof y of Q, then x and y together constitute a proof of P Q. · Or, more compactly: · Given x: P, y: Q then (x, y): P*Q.
More Inference Rules Another inference rule: · Assume we have a proof x of P. If we can then obtain a proof b of Q, then we have a proof of P Q. · Given [x: P] b: Q then fn (x: P) => b : P Q. More rules: · if x: P*Q then fst(x): P · if y: P*Q then snd(y): Q
Types and Proofs So, for example: fn (x: P*Q) => (snd(x), fst(x)) : P*Q Q*P We can develop a full metalanguage based on this principle of proofs as programs. · Codified in languages such as ML. · Typechecking gives us proofchecking!
ML-like Programming Languages The class of ML-like programming languages is based on this notion that proofs are programs and propositions are types. Research on this class of languages actually pre-dates the invention of computers by several decades!
