log in  |  register  |  feedback?  |  help
Logo
Beyond correct and fast: Inspection Testing
Friday, November 17, 2017, 12:00-1:00 pm Calendar
  • You are subscribed to this talk through .
  • You are watching this talk through .
  • You are subscribed to this talk. (unsubscribe, watch)
  • You are watching this talk. (unwatch, subscribe)
  • You are not subscribed to this talk. (watch, subscribe)
Abstract

Conventional testing is all about ensuring that your code behaves as it
should, and benchmarks allow you to ensure that it does so efficiently.
 But programmers, especially authors of carefully crafted libraries,
care about more than just correctness and performance:

When using generic programming, they care about what happens at
compile-time and what happens at run-time. When creating a stream
fusion (deforestation) library, they care about whether the compiler is
indeed eliminating all intermediate data structures. Programmers might
care about whether their code is allocation-free, using efficient
calling-conventions, or is free of branches. Often, a library makes
explicit promises of this kind to its users.

So far, the modus operandi in all these cases is that the programmer
manually inspects the (intermediate or final) code produced by the
compiler. This is not only tedious, but makes it very likely that some
change, either in the library itself or the surrounding eco-system,
breaks the library’s promised without anyone noticing.

The solution is – once the problem has been recognized – obvious: For
any such property, the programmer needs to be able to *declare* his
intent in a way that allows the compiler to *automatic* check it. This
insight gives rise to a new testing paradigm, which we call “Inspecting
Testing”.

In this talk I will discuss real-world examples (in the context of
Haskell) that demonstrate that there is a problem to be solved, clearly
define “Inspection Testing” and show how it can help to solve the
problems in our examples.

Bio

Joachim Breitner has received his PhD in computer science from the
Karlsruhe Institute of Technology for his work of not only devising and
implementing the “Call Arity” analysis and transformation in the
Haskell compiler GHC, but also proving it to actually be an
optimization in the theorem prover Isabelle. This shows his main areas
of interest: Design and implementation of functional programming
languages, and interactive theorem proving. He is currently a post-doc
at the University of Pennsylvania, where he joined the DeepSpec
project.

This talk is organized by Niki Vazou