CIS 500: !SOFTWARE FOUNDATIONS Lecture 1 Stephanie Weirich Fall, 2014 CIS 500: Fall 2014Administrivia • Instructor: Stephanie Weirich ! Office hours: Tomorrow 10-12, TBA in general! Levine 510 • TAs: – Arthur Azevedo de Amorim! Office hours: TBA – Justin Chiu! Office hours: TBA • Location: Tues LRSM AUD, Thurs Levine 101 • E-mail: [email protected] • Web site: http://www.seas.upenn.edu/~cis500 • Canvas: https://upenn.instructure.com • Piazza: http://piazza.com/upenn/fall2014/cis500 CIS 500: Fall 2014 Dr.$Weirich$will$be$in$Sweden$$for$ICFP$Aug$30;Sep$5.$$Arthur$will$lecture$next$week.$Resources • Course textbook: Software Foundations – Electronic edition tailor-made for this!class – Use the version available from the cis500 course web pages. • Additional books: – Types and Programming Languages!(Pierce, 2002 MIT Press) – Interactive Theorem Proving and Program Development!(Bertot and Castéran, 2004 Springer) – Certified Programming with Dependent Types!(Chlipala, electronic edition) CIS 500: Fall 2014Course Policies • Prerequisites: – Significant programming experience – Mathematical sophistication – Undergraduate functional programming or compiler class Grading: • 24% Homework ~12 weekly assignments • 18% Midterm I (tentatively) Sep 30th • 18% Midterm 2 (tentatively) Nov. 6th • 36% Final Thursday, Dec 18th 9-11AM • 4% Class participation ⇒ Lecture attendance is crucial! “Regular” and “Advanced” tracks (graded separately). CIS 500: Fall 2014“Regular” vs. “Advanced” Tracks • “Advanced” track: – More and harder exercises – More challenging exams. – It is a superset of the “regular” material. • All students start in the advanced track by default. • Students who wish to take CIS 500 for WPE I credit (Ph.D.) must take the advanced track. • Students may switch from advanced to regular track at any time. – Notify the course staff in writing. – The change is permanent after the first midterm. • Students wishing to switch (back) to the advanced track: – Must do so before the first midterm exam. – Must make up all the advanced exercises (or accept the grade penalty). • Only students taking the advanced track are eligible for an A+. CIS 500: Fall 2014Participation Policy • Class attendance is mandatory. • We will be using “clickers” for – in-class mini quizzes – in-class polls about course material • TurningPoint clickers use will be your attendance record. • For next time: buy a clicker. • Any TurningPoint RF clicker will work, see note on course website. CIS 500: Fall 2014Homework Policies • Homework is to be done individually. • Homework must be submitted via Canvas • Homework that is late is subject to: – 25% penalty for 1 day late – 50% penalty for 2 days late – 75% penalty for 3 days late • Homework is due at 8:00pm on the due date (generally Thurs.). • Advanced track students must complete (or try to complete) all non-optional exercises. – Missing “advanced” exercises will count against your score. • Regular track students must complete (or try to complete) all non-optional exercises except those marked “advanced”. – Missing “advanced” exercises will not count against your score. – (But may help in your understanding of the material) CIS 500: Fall 2014SOFTWARE FOUNDATIONSLOGICAL FOUNDATIONSA: How do we know something is true? B: We test it out A: But that isn’t truth; testing can only give us evidence. How do we know something is true? B: We prove it A: How do we know that we have a proof? B: We need to define what it means to be a proof. !A proof is a logical sequence of arguments, starting from some initial assumptions A: How do we know that we have a valid sequence of arguments? Can any list be a proof? All humans are mortal All Greeks are human I am a Greek B: No, no, no! We need to think about how we think…. CIS 500: Fall 2014First we need a language… • Gottlob Frege: a German mathematician who started in geometry but became interested in logic and foundations of arithmetic. • 1879 Published “Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens” (Concept-Script: A Formal Language for Pure Thought Modeled on that of Arithmetic) – First rigorous treatment of functions and quantified variables – ⊢ A, ¬A, ∀x.F(x) – First notation able to express arbitrarily complicated logical statements CIS 500: Fall 2014 Gottlob Frege !1848-1925 Images in this & following slides taken from Wikipedia.Formalization of Arithmetic • 1884: Die Grundlagen der Arithmetik (The Foundations of Arithmetic) • 1893: Grundgesetze der Arithmetik (Basic Laws of Arithmetic, Vol. 1) • 1903: Grundgesetze der Arithmetik (Basic Laws of Arithmetic, Vol. 2) • Frege’s Goals: – isolate logical principles of inference – derive laws of arithmetic from first principles – set mathematics on a solid foundation of logic CIS 500: Fall 2014 The plot thickens… Just as Volume 2 was going to print in 1903, !Frege received a letter…Bertrand Russell • Russell’s paradox: • Frege’s language could derive Russell’s paradox. • Frege’s logical system could derive anything. Oops. CIS 500: Fall 2014 Bertrand Russell ! 1872 - 1970 1. Set comprehension notation: { x | P(x) } “The set of x such that P(x)” 2. Let X be the set { Y | Y ∉ X }. 3. Ask the logical question: ! Does X ∈ X hold? 4. Paradox! If X ∈ X then X ∉ X. If X ∉ X then X ∈ X.#Addendum to Frege’s 1903 Book CIS 500: Fall 2014 “Hardly anything more unfortunate can befall a scientific writer than to have one of the foundations of his edifice shaken after the work is finished. This was the position I was placed in by a letter of Mr. Bertrand Russell, just when the printing of this volume was nearing its completion.” – Frege, 1903Aftermath of Frege and Russell • Frege came up with a fix, but it made his logic trivial… • 1908: Russell fixed the inconsistency of Frege’s logic by developing a theory of types. • 1910, 1912, 1913, (revised 1927):!Principia Mathematica (Whitehead & Russell) –