Skip to main content
BOB Konferenz 2018

Logo of BOB Konferenz 2018 BOB Konferenz 2018

23rd February 2018

Berlin, Germany

Part of the BOB series

Schedule for

  1. in Main Room

    Keynote: A Language for Making Movies

    Video is a language for making movies. It combines the power of a traditional video editor with the capabilities of a full programming language. Video integrates with the Racket ecosystem and extensions for DrRacket to transform it into a non-linear video editor.

    Racket enables developers to create languages (as libraries) to narrow the gap between the terminology of a problem domain and general programming constructs. The development of the video editing language cleanly demonstrates how the Racket doctrine naturally leads to the creation of language hierarchies, analogous to the hierarchies of modules found in conventional functional languages.

  2. Introductory Haskell

    Haskell is an elegant and fascinating language that has made functional programming practical. In this tutorial, we will discover some key concepts of Haskell in an interactive tour tailored to the interests of the audience.

    Possible topics include:

    purity
    lazy evaluation
    recursion
    higher-order functions
    algebraic data types
    polymorphism
    type classes
    some common abstractions
    type driven development
    

    Since 90 minutes are not enough to learn all details of a language, the main goal of this tutorial is to provide an overview of what makes Haskell special and serve as a starting point from which participants can continue learning on their own.

    No previous knowledge about functional programming is assumed, but some experience with programming in general might be helpful. To follow along and try their own ideas, participants will need the GHC compiler (which can be installed as part of the Haskell Platform). Please make sure to set it up beforehand so we can start on time! You should be able to start the interactive interpreter GHCi.

  3. Web-Entwicklung mit Clojure

    Clojure ist ein Lisp-Dialekt auf der JVM, somit elegant und mächtig zugleich. In dem Tutorial fangen wir mit einer Einführung in Clojure an, um dann einen einfachen Web-Service mit Datenbankanbindung in Clojure zu entwickeln, den man als Grundlage für weitere Arbeiten mit Clojure verwenden kann.

    Wer das Tutorial am eigenen Laptop nachvollziehen will, sollte vorher Leiningen aufgesetzt haben:

    https://leiningen.org/

  4. Reactive Streaming with Akka Streams

    A lot of data processing can be decomposed into sequential stages of iterating and aggregating. The usual pattern is to retrieve data, apply some function to it, and store the result away for the next processing stage. In practice, this is usually complicated by the need to handle errors, to execute parts asynchronously or in parallel, to merge data streams, and to wait for blocking I/O. As the amount of data increases, resilience against congestion, overflow and concurrency problems becomes more and more important, and at the same time harder to manage.

    Akka-Streams offers a powerful framework for asynchronous pipeline processing with memory-safety through backpressure. Data flow is modelled as a graph of Source, Sink and Flow elements that compose in a type-safe way. This approach hides all the details of rate limiting, buffering, pipelining, and asynchronicity, while retaining their explicit semantics. And it profits from the large ecosystem that already exists around the Akka framework!

  5. Testing monadic programs using QuickCheck and state machine based models

    I would like to show how one can apply property based testing to “real-world” programs, such as a CRUD web server application. I’m interested in properties about the system as a whole, not merely some pure parts of it (e.g. serialising and deserisalising to and from JSON).

    To achieve this I’ve implemented a Haskell library on top of QuickCheck that makes it possible to specify the correctness of the system using pre- and post-conditions over a state machine model a la Erlang’s proprietary version of QuickCheck.

    I’ll explain how the library works and demo how one can use it to specify the correctness of and test a simple CRUD web application. In the process we will expose bugs in the program logic as well as a race condition.

    Finally, I’ll compare and contrast the approach presented to other similar tools: Z/B-method/Event-B, TLA+, and Jepsen.

  6. Funktionale Datenstrukturen

    Mal ganz unabhängig von den Problemen mit der Parallelität ist es auch einfach so sehr oft eine gute Idee, seine Objekte und Datenstrukturen unveränderlich zu halten. Wie sich dies im Zusammenhang mit Collections bei einer Liste bewerkstelligen lässt, ist wohl auch weitestgehend bekannt. Aber wie steht es um die anderen Datenstrukturen, etwa einer Menge, einer Map, einem Array oder einer Queue?

    Dieser Vortrag beschäftigt sich mit abstrakten Datentypen und implementierenden, rein funktionalen, „persistenten“ Datenstrukturen. Dabei wird nicht nur gezeigt, wie sich deren Performance von ihren veränderbaren Verwandten unterscheiden, sondern insbesondere auch gezeigt, wie man sich der Objektorientierung bedienen kann, um jene möglichst effizient zu gestalten.

  7. When one beyond-mainstream technology is not enough: Combining program verification with component-based architectures

    Fuzzing. Bug bounties. ASLR. Code reviews. Despite the immense efforts put into improving the robustness of our software and the security of our systems, we don’t seem to make good progress here. Have a look at a recent update to your favorite smartphone OS. Every single month, dozens of flaws get fixed. But even more are still lurking in the code bases. Many of them allow for total system compromise. What is the reason that the situation does not seem to improve?

    We argue that it’s the due to lacking approaches at the architecture level as well as the implementation level. Consequently, the problem has to be addressed at those two levels: Firstly, our systems need to be structured such that most complexity is in untrusted components which cannot affect system security. Secondly, for the much smaller trusted portions we need to establish formal correctness arguments.

    In this talk, we present our approach to building trustworthy mobile OS. We combine the novel system architecture of the Genode OS framework with the SPARK technology for high-reliability applications.

  8. Terminal GUIs with Haskell: vty and brick

    For interactive full-screen terminal applications, the usual go-to ecosystem is plain C with the ncurses library. However, also the Haskell ecosystem has a lot to offer: vty, a high-level combinator library for formatting and arranging text elements on a terminal screen. And building on top of vty we have brick, a library for layouting terminal applications from widgets. Where you need to tell ncurses exactly to »put the cursor there and print a char«, the declarative approach of these libraries is much safer and easier to manage.

    After a short introduction to the basics of event handling and terminal rendering in Haskell, we’re going to play »Pong« on the terminal!

  9. in Main Room

    Einführung in Agda

    Viele Programmierer führen nur ungern Beweise: Agda verwendet das Curry-Howard-Prinzip “Beweise sind Programme”, so dass es ausreicht ein typkorrektes Programm zu schreiben um zu zeigen, dass ein Programm seine Spezifikation erfüllt.

    Agda ist eine funktionale Programmiersprache mit abhängigen Typen und gleichzeitig ein interaktives Beweissystem. Das mächtige Typsystem erlaubt, auch substanzielle Eigenschaften direkt ins Programm zu schreiben.

    Nach einer Einführung in die funktionale Programmierung mit Typen und das Curry-Howard-Prinzip führen wir anhand von Beispielen die wichtigsten Features von Agda vor. Zum Abschluss beleuchten wir einige Anwendungen von Agda und geben Hinweise auf Informationsquellen zum Thema.

  10. FIX-Engine in zwei Wochen

    Durch stätig fortschreitende Globalisierung und Regulierung herrscht in der Finanzwelt einerseits der enorme Kostendruck, andererseits die wachsende Kommunikationsprotokollevielfalt. Unter diesen Umständen muss der Entwickler bei der Implementierung der Börsenschnittstellen sehr effizient sein. Meistens stellen die Börsenbetreiber die Beschreibungen der Schnittstellen und Datenformate im XML-Format zur Verfügung, so dass die Konverter automatisch generiert werden können. Um anschließend die Korrektheit des generierten Programms überprüfen zu können, bietet sich Property Based-Testing an. Die Ziel-Eigenschaft ist dabei sehr einfach und gleichzeitig sehr mächtig - „decode(encode (A)) == A“. In dem Vortrag wird erläutert, worauf es dabei ankommt und was insbesondere beachtet werden muss. Als Beispiel wird eine Erlang-Implementierung einer FIX-Engine angesehen. Dabei werden sowohl die persistenten (Codegenerierung vor der Laufzeit) als auch dynamischen (Parsetransform) Varianten der generativen Programmierung vorgestellt, sowie deren Vor- und Nachteile behandelt.

  11. Formally Specifying Blockchain Protocols using the Psi Calculus

    Blockchains are distributed systems, with actors that adhere to agreed-upon protocols. The protocols ensure that the systems performs as desired, even when some of the actors behave dishonestly.

    Since the integrity of such a system can protect hundreds of millions of dollars, cryptographers spend great effort on designing the protocols, and proving correctness guarantees under well-specified threat models. The implementation of the actual systems running those protocols is then performed by software engineers. These two activities require different skillsets, as well as different levels of abstraction. Bridging this gap while preserving the correctness guarantees is a non-trivial task.

    At IOHK, we use the Psi calculus to translate the cryptographic protocols described in research papers (main protocol here, related papers here) into a formal language, producing a machine-readable, executable specification. This has multiple benefits:

    • It creates a common language for the researchers and engineers.
    • It forces the specification to be complete and unambiguous.
    • It allows simulations, including performance simulations, of the systems before they are fully implemented.

    The leap that leads from the research paper to the implementation can then be replaced by a larger number of small steps, each refining the specification and adding more details and design decisions. It is then feasible to show that the implementation matches the paper, by verifying that each of these steps.

  12. Vertikale Organisation - da muss sich was um 90° drehen im Kopf!

    n einer herkömmlichen Stab-Linien-Organisation mit ISO/OSI geschichteter IT und Produktentwicklung trifft man oft Stillstand und bis zur Unbeweglichkeit durch Abhängigkeiten verknotete Roadmaps an. Daher ist es wenig verwunderlich, dass hier alte, schwer ablösbare IT-Produkte schwerfällig im Betrieb sind. In einer vertikalen Organisation arbeiten cross-funktionale Teams an einem kompletten Produkt-Stack von der Kundenschnittstelle bis zum Betrieb. Jedes dieser Teams ist für einen fachlichen Bereich, eine sogenannte Domäne, verantwortlich. Die verschiedenen fachlichen Domänen werden dabei im Sinne einer funktionalen Modularisierung durch voneinander getrennte Systeme umgesetzt. Das share-nothing Prinzip führt zu größtmöglicher Unabhängigkeit der Systeme und Teams. Dies minimiert den Kommunikationsaufwand zwischen Teams und die Anzahl der Stakeholder pro Team. Die nötige übergreifende Kommunikation findet über horizontal angelegte Communities of Practice statt. Beispiele solcher Organisationen sind XING, Otto, Breuninger, Spotify.

  13. GRiSP, Bare Metal Functional Programming

    We present a new hardware platform called GRiSP. It allows you to run Erlang on bare metal hardware, without a kernel. It is specifically made for rapid prototyping of Internet of Things devices and has a wide range of hardware access ports. We will introduce the hardware, talk about how Erlang runs natively on the device and give an overview of some of the research that the platform is involved in. We are a member of the LightKone H2020 EU project doing research on edge computing, including for example Conflict-free Replicated Data Types (CRDTs). The GRiSP board will be used as a prototyping edge device by the researchers for IoT applications and by us for use cases ranging from “industry 4.0” smart conveyor belts to smart metering. A live demo will be showcased showing of some features of the device and how to interact with hardware components.

  14. Graphical User Interfaces in Haskell with Threepenny

    Purely functional programming languages like Haskell do not allow mutable state or other side effects in plain functions. A popular misconception says that this could make real-life tasks like programming graphical user interfaces (GUI) more difficult. This is not the case. The aim of this tutorial is to show that Haskell is, in fact, well-suited for GUI programming.

    In this tutorial, I will give a hands-on introduction to writing GUI applications with Haskell using my GUI library “Threepenny”. This library is easy to install, because it uses the web browser as a display. First, I will give a brief overview of the library architecture. Then, I will present the basic concepts of GUI programming in Haskell by walking through a few example programs. At the end, we will look at how the paradigm of functional reactive programming (FRP), a radical departure from the traditional imperative paradigm, can simplify GUI programming.

  15. A Tutorial on Liquid Haskell

    Liquid Haskell is a preprocessor for GHC (the primary Haskell compiler) that allows the programmer to equip a program with more sophisticated type annotations. An automatic external theorem prover such as Z3 is then used to prove the program type-correct with respect to these extra annotations.

    The language of types supported by Liquid Haskell is based on refinement types, and allows types to be restricted to certain values or properties of their values. For example, we can define the type of integers between 0 and 10, or the type of lists that have a particular length. We can establish pre- and postconditions of functions using refinement types, potentially proving rather sophisticated properties.

    In this tutorial, I will introduce Liquid Haskell, explain how it works, and what can (and cannot) be expected of it. We will look at a number of examples and see how they can be equipped with more precise types than Haskell would normally allow.

  16. in Main Room

    Understanding the realtime ecosystem

    It’s 2018, the time of data-driven realtime applications. With the applications increasingly becoming data dependent, realtime technology has suddenly gained momentum as opposed to a steady pace through the previous years. It is important to understand the main underlying concepts that make an application work in realtime. This talk will walk the audience through concepts such as data-sync, pub/sub, websockets, etc while clearly underlining the differences between other technologies, paradigms and protocols. This talk will be summarized with a live example of how realtime systems truly function using deepstream.io, an open realtime server that provides all the realtime features discussed right out of the box, thus limiting the developer’s role to use case specific implementation.

  17. New Hasql - a native Haskell Postgres driver faster than C

    In the recent years Haskell has matured into a great tool for database-driven applications with lots of open-source projects offering integration with all kinds of databases. There’s a special amount of competition happening in the area of integration with PostgreSQL, with multiple projects offering different features.

    Hasql is a project, which aims to squeeze the maximum performance, while still offering a nice and mathematically correct layer of abstraction. It is already known as the fastest driver in Haskell and powers the Postgrest project, which has 10k stars on GitHub.

    The upcoming version of Hasql makes another leap in performance by completely reimplementing the communication with the backend. Now it directly uses the binary protocol instead of wrapping the “libpq” C library, which is used by the majority of Postgres libraries for all languages. Now Hasql has set the purpose to supersede “libpq” in performance altogether.

    In this talk I’ll give a detailed introduction into the library, core ideas behind it, its new features and will provide a tutorial on using it.

  18. in Main Room

    May contain DTraces of FreeBSD feat. Spectre

    Systems are getting increasingly complex and it’s getting harder to understand what they are actually doing. Even though they are built by human individuals they often surprise us with seemingly bizarre behavior. DTrace lights a candle in the darkness that is a running production system giving us unprecedented insight into the system helping us to understand what is actually going on.

    We are going implement strace-like functionality, trace every function call in the kernel, watch the scheduler to its thing, observer how FreeBSD manages resources and even peek into runtime systems of high level programming languages. If you ever wondered what software is doing when you are not looking, this talk is for you.

  19. Finite-state machines? Your compiler wants in!

    When modeling problem domains, we collect different possible states, legal transitions between states, and relevant data for each state. Finite-state machines emerge. To verify that programs are constructed correctly, and to have a living machine-verified documentation, we should let the compiler in on our trade secrets.

    In this talk we will look at motivations and examples of encoding finite-state machines, using the expressive type systems of Haskell and PureScript. We will see how they help us in implementing our model, and how they communicate a high-level design.

  20. in Main Room

    Hedgehog - QuickCheck, but better

    hedgehog is a Haskell library for writing property-based tests similar to the more established QuickCheck: instead of “when passed [3, 1, 2], this function returns [1, 2, 3]”, you write “when passed a list of numbers, this function returns a list with the same elements in order”. properties are tested on a range of random values and provide far wider test coverage.

    In this tutorial, you will get acquainted with the concepts of property-based testing and the specific benefits of hedgehog, like better error reporting and sound shrinking for free. With a little luck we’ll get as far as state machine testing like in the BOB QuickCheck talk.

    Some experience with software development and writing tests would be great. Knowledge of QuickCheck is not required. Material and exercises will be provided soon.

  21. EventStorming für Domain-Driven Design

    Wie wär’s, wenn wir einfach mal “Kommunikation” nehmen? – Viele Projekte kranken daran, dass die Kommunikation zwischen den Beteiligten nicht gut funktioniert, und zwar in vielerlei Hinsicht:

    • Die Projektverantwortlichen denken sich im Vorfeld selbst was aus, anstatt mit Problemen zu den Entwicklern zu kommen. (“Das ist so doch bestimmt am einfachsten!”)
    • Die Entwickler denken sich bei Unklarheiten selbst was aus, anstatt die Fachbereichler um Klärung zu bitten. (“Das kann doch nur so gemeint sein!”)
    • Derselbe Begriff wird für verschiedene Dinge benutzt
    • Verschiedene Begriffe werden für dasselbe Ding benutzt
    • Probleme oder Defekte werden in der Konzeptionsphase übersehen oder ignoriert und tauchen erst nach mehrmonatiger teurer Entwicklung auf

    Wer wissen möchte, wie alle Projektbeteiligten gemeinsam es schaffen können, diese Fallen zu umschiffen und den Weg zu bahnen zu gut implementierbarer Software, und wer das Ganze auch noch hautnah erleben möchte, den lade ich ein zu meinem Workshop “EventStorming für Domain-Driven Design”.

  22. Engineering TCP/IP with logic

    TCP/IP is a complex protocol, which is specified in a series of RFCs. Each RFC is written in English prose, and interpreted differently by different people. Nevertheless, TCP/IP is a widely deployed network protocol nowadays, a lot of people depend on it.

    In this talk, I will present a formal model of TCP/IP (developed 2000-2009 and refurbished since 2016), how it can be used to validate the FreeBSD TCP/IP stack, and what we learned while writing it. It is modelled as a label transition system, including timers, retransmission, etc. Hundreds of transition rules are defined to cope with the little details of TCP/IP. We use symbolic execution to validate a trace, which is produced by running a test on a TCP/IP stack, using backtracking which is required to validate some traces.

    While formalising TCP in HOL4, roughly 3 dozen anomalies have been discovered, and partially reported upstream. The development of the formal model also lead to an extended and more correct state machine on top of the initial TCP/IP RFC 793.

    The resulting model spans over 350 pages, and contains lots of documentation. The pdf is rendered directly from the HOL4 source, the tool HOLDoc was engineered which combined the transition rules and comments into latex code. A recent draft is available at http://www.cl.cam.ac.uk/~pes20/Netsem/paper3.pdf.

    This is joint work with Peter Sewell, Michael Norrish, Tom Ridge, earlier contributors are Steve Bishop, Matthew Fairbairn, Michael Smith, and Keith Wansbrough. The model is available under the 2 clause BSD license at https://github.com/PeterSewell/netsem.

    The project website is http://www.cl.cam.ac.uk/~pes20/Netsem/index.html

  23. Implications of Functional Programming on Human Rights Work

    The human rights sector is increasingly complementing its more traditional forms of research with data and computational methodologies. This has lead to a demand for tools that activists can integrate in their daily data collection and documentation work. This presentation will explore how choices in software construction impact their work.

    A central focus in developing software for the human rights sector lies in its focus on adaptability and re-usability to ever changing realities of activists on the ground. Concepts such as immutable data and pure functions are already very beneficial. However, equipping this sector with tools that are based on functional abstractions and techniques can have even further advantages. The concepts and abstractions we use to build software influence the processes people form around those tools.