Strangeloop 2012 presentation with Daniel Spiewak

Published on: **Mar 4, 2016**

Published in:
Technology Business

- 1. 9p p 2 Pontiﬁcating
- 2. Programming is Hard
- 3. Who watches the watchers?
- 4. Let’s talk about veriﬁcation
- 5. XUnit
- 6. Standard Practice• We all use it• Most of us rely on it day to day• We seem to trust it implicitly
- 7. def test_example # create something to test obj = MyExampleObject.new(arguments) # program statement result = obj.example_method(arguments) # verification assert_equal("fact", result) #implicit teardownendit "must be an example" do obj = MyExampleObject.new(arguments) result = obj.example_method(arguments) result.should == factend
- 8. XUnit is Complected• It’s doing too much
- 9. XUnit is Complected• It’s doing too much• BDD is just XUnit with lots of bad English
- 10. XUnit is Complected• It’s doing too much• BDD is just XUnit with lots of bad English• Poor separation of the tester and testee
- 11. XUnit is Complected• It’s doing too much• BDD is just XUnit with lots of bad English• Poor separation of the tester and testee• What are you testing?
- 12. XUnit is Complected• It’s doing too much• BDD is just XUnit with lots of bad English• Poor separation of the tester and testee• What are you testing? • Are you sure?!
- 13. Your mock object is a joke; that object is mocking you. For needing it. – Rich Hickey
- 14. Coverage is a Lie• Too many false indicators of comprehensive veriﬁcation• We work really hard at the wrong things to achieve good coverage• “The Emperors new suit”
- 15. Always in Manual Drive• Devise, write, and maintain all cases• Edge cases are a (big) problem • Especially with simple functions• Example: Integer commutative law
- 16. Generative Testing
- 17. Logic #fail 9x f (x) 6= expect(x) ) bugs9x f (x) = expect(x) ) ¬bugs
- 18. Logic #fail 9x f (x) 6= expect(x) ) bugs9x f (x) = expect(x) ) ¬bugs
- 19. Logic #fail 9x f (x) 6= expect(x) ) bugs9x f (x) = expect(x) ) ¬bugs
- 20. Generative Testing• Developing test cases is hard• We have computers!• Deﬁne your domain, auto-generate inputs• Write less, test more• Find edge cases automatically!
- 21. Generative Testing• Developing test cases is hard• We have computers!• Deﬁne your domain, auto-generate inputs• Write less, test more• Find edge cases automatically! • (money back guarantee)
- 22. (defspec integer-commutative-laws (partial map identity) [^{:tag `integer} a ^{:tag `integer} b] (if (longable? (+ a b)) (assert (= (+ a b) (+ b a) (+ a b) (+ b a) (unchecked-add a b) (unchecked-add b a))) (assert (= (+ a b) (+ b a)))) (if (longable? (* a b)) (assert (= (* a b) (* b a) (* a b) (* b a) (unchecked-multiply a b) (unchecked-multiply b a))) (assert (= (* a b) (* b a)))))
- 23. "integer commutative law" in { check { (x: Int, y: Int) => (x + y) mustEqual (y + x) (x * y) mustEqual (y * x) }}
- 24. Generative Testing• Real world cases?
- 25. Generative Testing• Real world cases? • Sparse trees
- 26. Generative Testing• Real world cases? • Sparse trees • Complex pre-conditions
- 27. Generative Testing• Real world cases? • Sparse trees • Complex pre-conditions• How many iterations?
- 28. Rice’s Theorem
- 29. […] there exists no automatic method thatdecides with generality non-trivial questionson the black-box behavior of computerprograms. – Wikipedia
- 30. Rice’s Theorem• You can never have enough assertions
- 31. Rice’s Theorem• You can never have enough assertions• All you can do is improve “conﬁdence” • (for some naïve deﬁnition thereof)
- 32. Rice’s Theorem• You can never have enough assertions• All you can do is improve “conﬁdence” • (for some naïve deﬁnition thereof)• Black box testing is a farce
- 33. Rice’s Theorem• You can never have enough assertions• All you can do is improve “conﬁdence” • (for some naïve deﬁnition thereof)• Black box testing is a farce• Partial function indistinguishable from total
- 34. def addGood(x: Int, y: Int) = x + y// egad!def addBad(x: Int, y: Int) = (x, y) match { case (0, 0) => 0 case (0, 1) => 1 case (1, 0) => 1 case (2, 3) => 5 case (100, 500) => 600}
- 35. Black Box Testing• Do we just…enumerate cases?
- 36. Black Box Testing• Do we just…enumerate cases?• When do we stop? (hint: never!)
- 37. Black Box Testing• Do we just…enumerate cases?• When do we stop? (hint: never!)• Can we assume edge cases are predictable?
- 38. Black Box Testing• Do we just…enumerate cases?• When do we stop? (hint: never!)• Can we assume edge cases are predictable?• What can we assume?
- 39. Black Box Testing• Do we just…enumerate cases?• When do we stop? (hint: never!)• Can we assume edge cases are predictable?• What can we assume?• It’s all undecidable, let’s go shopping
- 40. In the beginning…
- 41. An Axiomatic Basis for Computer Programming
- 42. Partial Correctness P {Q} R
- 43. Built on two ideas• Axioms • The foundation of proofs in our system (assignment, precendence, identity, etc)• Inference • Higher order ideas that use combinations of axioms to draw conclusions
- 44. It drove us to thinkabout consequence in program execution
- 45. Be Careful!¬9x 8y (y x)
- 46. Computers are ﬁnite! 8x (x max)
- 47. Real Example Commutative law x+y =y+x x⇥y =y⇥x
- 48. Rules of Consequence(` P {Q} R) ^ (` R S) ) (` P {Q} S)(` P {Q} R) ^ (` S P ) ) (` S {Q} R)
- 49. Our problems are solved!
- 50. Se e G are solved!Our problems ö del
- 51. Type Systems
- 52. Type Systems• Mildly controversial…
- 53. Type Systems• Mildly controversial…• Formal veriﬁcation…that you can’t disable!
- 54. Type Systems• Mildly controversial…• Formal veriﬁcation…that you can’t disable!• Part of the language (inextricably) • (yes, that is a deﬁnitional requirement)
- 55. Type Systems• Mildly controversial…• Formal veriﬁcation…that you can’t disable!• Part of the language (inextricably) • (yes, that is a deﬁnitional requirement)• Model correctness as consistency
- 56. G`t :T 0 P ROGRESS t ) t _ t is valueG`t :T t )t 0 P RESERVATION G`t :T 0
- 57. case class Miles(value: Int)case class Kilometers(value: Int)def launchMarsMission(distance: Miles) = { val kph = distance.value / (6 * 30 * 24) increaseSpeedToKPH(kph)}
- 58. trait Forall[CC[_]] { def apply[A]: CC[A]}trait ST[S, A] { def flatMap[B](f: A => ST[S, B]): ST[S, B]}object ST { def run[A]( f: Forall[({ type λ[S] = ST[S, A] => A })#λ]): A}
- 59. Correct by Construction• Incorrect algorithms fail to compile Call me Ishmael…
- 60. Correct by Construction• Incorrect algorithms fail to compile• Bugs are a thing of the past Call me Ishmael…
- 61. Correct by Construction• Incorrect algorithms fail to compile• Bugs are a thing of the past• Programmers herald new era Call me Ishmael…
- 62. Correct by Construction• Incorrect algorithms fail to compile• Bugs are a thing of the past• Programmers herald new era• Proﬁt? Call me Ishmael…
- 63. Curry-Howard• Types are logical propositions• Values are proofs of propositions• Type checking is testing logical validity• A system’s consistency is what is checked
- 64. -- Thm. Integer implies Walrustheorem :: Integer -> Walrustheorem a = theorem a
- 65. -- Thm. everything implies Walrustheorem :: forall a . a -> Walrustheorem a = theorem a
- 66. -- Thm. everything is true!theorem :: forall a . atheorem = theorem
- 67. Gödel• Self-referentiality is a problem
- 68. Gödel• Self-referentiality is a problem • Hello, Strange Loop!
- 69. Gödel• Self-referentiality is a problem • Hello, Strange Loop!• Incomplete or inconsistent
- 70. Gödel• Self-referentiality is a problem • Hello, Strange Loop!• Incomplete or inconsistent• Some valid programs cannot be typed
- 71. Gödel• Self-referentiality is a problem • Hello, Strange Loop!• Incomplete or inconsistent• Some valid programs cannot be typed• Strong normalization helps • (avoids the need for recursive types!)
- 72. System F• Strongly normalizing λ calculus
- 73. System F• Strongly normalizing λ calculus• Statically typed, and complete!
- 74. System F• Strongly normalizing λ calculus• Statically typed, and complete! • All valid programs can be typed
- 75. System F• Strongly normalizing λ calculus• Statically typed, and complete! • All valid programs can be typed • No invalid programs can be typed
- 76. System F• Strongly normalizing λ calculus• Statically typed, and complete! • All valid programs can be typed • No invalid programs can be typed• Immensely expressive (lists, numbers, etc)
- 77. System F
- 78. System F• Not expressive enough
- 79. System F• Not expressive enough• Cannot bootstrap its own compiler
- 80. System F• Not expressive enough• Cannot bootstrap its own compiler• Many valid programs have no encoding
- 81. System F• Not expressive enough• Cannot bootstrap its own compiler• Many valid programs have no encoding• Not Turing-complete! (trivially so)
- 82. Static Typing• Can’t even answer some basic questions
- 83. Static Typing• Can’t even answer some basic questions• Fails to deﬁnitively answer any questions • …for Turing-complete calculi
- 84. Static Typing• Can’t even answer some basic questions• Fails to deﬁnitively answer any questions • …for Turing-complete calculi• Arms race of inconvenience
- 85. Static Typing• Can’t even answer some basic questions• Fails to deﬁnitively answer any questions • …for Turing-complete calculi• Arms race of inconvenience• Guardrails on a sidewalk
- 86. add :: Integer -> Integer -> Integeradd x y = x + y
- 87. add :: Integer -> Integer -> Integeradd x y = x + yadd :: Prime -> Prime -> Integeradd x y = x + y
- 88. (define (add x y) (+ x y))
- 89. (define (add x y) (+ x y))(module strangeloop racket (provide (contract-out [add (->* (prime? prime?) () integer?)])))
- 90. (define (divisible? i m) (cond [(= i 1) true] [else (cond [(= (remainder m i) 0) false] [else (divisible? (sub1 i) m)])]))(define (prime? n) (divisible? (sub1 n) n))
- 91. (require strangeloop)(add 7 7);; > 14
- 92. (add 4 7);; > add: contract violation;; expected: prime?, given: 4;; in: the 1st argument of;; (-> prime? prime?;; integer?);; contract from: strangeloop;; blaming: top-level;; at: stdin::79-82;; context...:
- 93. But like everythingelse, it suffers from deﬁciencies...
- 94. Before Contract Application(time (add 492876847 492876847));; > cpu time: 0 real time: 0 gc time: 0;; 985753694
- 95. Before Contract Application(time (add 492876847 492876847));; > cpu time: 0 real time: 0 gc time: 0;; 985753694 After Contract Application(time (add 492876847 492876847));; > cpu time: 15963 real time: 15995 gc time: 0;; 985753694
- 96. Runtime issues canmake contracts a non-starter for production code
- 97. It’s All Bunk• Black-Box veriﬁcation is insufﬁcient
- 98. It’s All Bunk• Black-Box veriﬁcation is insufﬁcient• White-Box veriﬁcation is undecidable
- 99. It’s All Bunk• Black-Box veriﬁcation is insufﬁcient• White-Box veriﬁcation is undecidable • …in general!
- 100. It’s All Bunk• Black-Box veriﬁcation is insufﬁcient• White-Box veriﬁcation is undecidable • …in general!• Constrain the domain
- 101. Functional Style• Write your code in a functional style• It is constraining…that’s the point!• FP is easier to reason about • (both formally and informally)• Easier to test, and easier to verify
- 102. Programming: The Good Parts
- 103. References• From System F to Typed Assembly Language• An Axiomatic Basis for Computer Programming• Hoare Logic and Auxiliary Variables• The Underlying Logic of Hoare Logic• Applying Design by Contract• Proof Carrying Code• Uniform Proofs as a Foundation for Logic Programming• Safe Kernel Extensions Without Run-Time Checking