Skip to main content
BOB 2019

Logo of BOB 2019 BOB 2019

22nd March 2019

Berlin, Germany

Part of the BOB series

Schedule for

  1. in Main Room

    Keynote: High-Peformance Haskell

    Functional languages are becoming increasingly popular, not least due to their high level of abstraction, reuse, and compositionally. By conventional wisdom, these features discourage their use for performance critical applications as they can come at the cost of lower efficiency. However, as demonstated by a number of new functional high-performance systems, we can make abstraction work for us in this space, exploiting the absence of uncontrolled side effects and the way they expose computational and communication patterns to aggressively optimise and generate highly efficient code

    The Haskell embedded DSL Accelerate is such a language. It enables application programmers with relatively little knowledge of parallel computing to write programs accelerated by multi-core CPU and GPU architectures, even beating hand optimised code for typical applications. In this talk, I will give an overview over programming in Accelerate, demonstrate some applications, and show how advanced features of the Haskell type system, like type families, play a crucial role in the implementation.

  2. in Tutorials #1

    Introduction to Web Development in Racket

    Racket is a Lisp that strives not only to be a best-in-breed environment for language-oriented programming; it’s also a great language for doing systems programming. In particular, Racket comes out-of-the-box with an HTTP server and a potpourri of libraries and DSLs for web development. For some time now, pretty much every language has had such feature, so what makes Racket different and worth consideration? A killer feature that distinguishes Racket from other frameworks and languages it is support for continuations and their clever use to make a full-fledged language for web programming, which help make REST and allied concepts such as HATEOAS automatic. The aim of this tutorial is to give the audience an impression of what web programming in Racket looks like by building a little HTTP API. A Racket package will be made available with which you can hack along with the teacher as we proceed through the tutorial.

  3. in Tutorials #2

    Learn FP with Code Katas

    Functional programming helps you reason about and test your code by breaking it into self contained pieces in pure functions. In this workshop you will be given a code kata and a set of constraints which train pair programming and functional thinking such as ping pong, navigator-driver, verbs instead of nouns. Each pair will pick up a language which supports functional programming and a constraint based on their self evaluated experience level. The idea is to use constraints to trigger creative problem solving.

    Please bring your laptop which should be ready for development, with everything you need installed i.e. IDE and unit testing framework for languages such as Scala, Haskell, Clojure. Make sure it is set up properly by having a new project with a failing test. The workshop assumes basic programming skills and participants should be already able to solve problems using them. You can consider this a mini version of a coderetreat.

  4. in Talks #1

    Applicative DSLs

    Monadic DSLs are ubiquitous in functional programming: Parser combinators, build systems, test data generators (like QuickCheck’s Gen) are usually monadic, and »Free Monad + Interpreter« is a well-known pattern for building DSLs. Monads allow a great deal of flexibility for DSL embedding, and come with a rich interface of generic combinators. In comparison, Applicatives seem quite restricted at first glance. On the other hand however, Applicatives compose and parallelize easily, and provide several additional benefits, as we will see. Are these worth the restrictions?

    In this talk, we are going to explore libraries like optparse-applicative that use an applicative DSL for extra benefit, and show the design of an applicative DSL by the example of an Applicative test data generator library.

  5. in Talks #2

    Checking Musical Correctness

    Music theorists have a questionable history of taking tendencies observed in European musics and deploying them as prescriptive rulesets. Fortunately, musicians break these rules whenever it suits them. In fact, cognitive science suggests that rulebreaking and manipulating audience expectations is fundamental to how music is able to provoke emotion. But in the universe of algorithmic music, we can, if we choose, use software correctness techniques like schemas and types to enforce musical rules. This gives rise to a dilemma. If we make illegal states unrepresentable, do we make innovative states unimaginable? This talk will attempt to resolve the dilemma using a practical reconciliation between Paul Hudak’s Haskell school of expression and David Huron’s psychological theory of expectations.

  6. in Talks #2

    Modern SQL

    Purely relational SQL has been abandoned in 1999. Since then, SQL has got many non-relational features for problems that are hard to solve with relational algebra. Today, SQL is Turing complete, can process graphs, has semantic understanding of XML and JSON, is able to automatically keep historic versions, can analyze time series using regular expressions and much more.

    This presentation demonstrates what modern SQL can do for you. It compares two different approaches to common problems: a purely relational one and the modern SQL approach. You will see that modern SQL databases are the Swiss Army Knives of persistence which allow up to react quickly when requirements change.

    In this session, developers and software architects of all levels gain a better understanding where SQL is today so that they are able to make more educated decisions. A lot has happened since SQL-92!

  7. in Talks #1

    Inspection Testing

    A Promise Checked is a Promise Kept

    Some high-quality Haskell libraries, including old friends like text and new kids on the block like generic-lens, promise that the abstractions provided by these libraries are actually free and will be completely dissolved by the compiler. In the case of text the promise is that certain pipelines of text-processing functions will be optimizes (“fused”) to never allocate a full text value; generic-lens promises that its generically derived lenses are, after optimization, identical to handwritten ones.

    But, in practice, these promises often don’t hold. They held at some point in the past, when the author checked them manually, but later versions regressed.

    This problem can be fixed with inspection-testing, a Haskell library and plugin to the compiler that allows you to explicitly state what you expect from the compilers optimizations, and have the compiler check that it actually happens. This can be used by library authors to test their promises, but also by users to learn more about what the compiler does with their code.

    In this talk, you will discover the tale of broken promises in commonly used Haskell libraries, and you will learn how these promises can be checked automatically using inspection-testing.

  8. in Tutorials #1

    Clojure, Getting Your Feed Wet

    Ever wanted to try using Clojure? Never got the time? This is an occasion!

    Coming from a mainstream language programming background (Java), learning a language like Clojure is like hitting your head on the wall… repeatedly.

    After a time, however, pieces seem to fall into place, and the magic happens: I started to reason in terms of data processing, and not in terms of objects anymore. If you want to come with me on my journey of learning Clojure as an OOP guy, I’ll be happy to show you strange beasts such as Dynamic Dispatch, Threading, Contract-Based Programming, and much much more.

  9. in Tutorials #2

    MirageOS: building minimized special-purpose unikernels

    Unikernels are specialized services, where the runtime binary (process, virtual machine) only contains the necessary libraries. This reduces the attack surface drastically (around two orders of magnitude). MirageOS is a unikernel project that uses OCaml, which also reduces the attack vectors (memory safety, type safety). MirageOS does not contain any process management, neither virtual memory – the entire unikernel is executed in single address space. The cooperative multitasking library lwt is used at the base.

    MirageOS can be deployed to various modern hypervisors: Xen, Linux KVM, FreeBSD BHyve, OpenBSD VMM, virtio, as well as to the Genode microkernel-based operating system framework and the separation kernel Muen. It can also be run as a unix process with rather restrictive seccomp filters (less than 10 syscalls needed). It runs on X86-64, ARM64 (Raspberry PI), ESP32; RISC-V support is along its way.

    Apart from core Internet Protocols (TCP/IP, DHCP, DNS, HTTP), security protocols (TLS, OpenPGP, OTR), and branchable distributed storage (implementing the git protocol) for persistency, several applications are work-in-progress:

    - Calendar and address book (CalDAV/CardDAV) storing data in a remote git repository
    - EMail (MIME encoding/decoding, SMTP, IMAP)
    - Firewall
    - VPN Gateway
    

    In this tutorial, first I’ll briefly introduce the benefits of MirageOS and the programming environment - the mirage command line utility takes care of target-specific dependency, initialization order, etc. by generating code. Afterwards, we’ll dig deep down further examples.

  10. in Talks #2

    Programmation en Logique

    Prolog is one of the most underrated programming languages around; possibly because of its strange syntax and the unusual paradigm. But it is a very nice special-purpose programming language. In this talk, I would like to introduce Prolog’s programming model, showcase some programming domains in which Prolog allows for very concise, elegant programs, and finally describe how it can also be used as a general-purpose tool.

  11. in Talks #1

    Logic in the Service of System Configurations

    Programming is glamorous; everyone has ideas for how it should be done better. System configuration, in contrast, lacks panache; it seems to consist mainly of fiddling with lots of little settings across devices. However, configuration actually performs a very difficult task: the devices are heterogenous, they work at different levels of abstraction (databases, servers, networks), and they form a distributed system that must act in concert to achieve a subtle (often unstated) goal. Indeed, many security and correctness problems stem not from incorrect programs (for which people constantly produce new verifiers) but rather from subtle configuration errors.

    There are several modalities of action: e.g., verification (given a configuration and a property, does the configuration match the property?); differential analysis (given two configurations, how are they different?); and synthesis (given a specification, can we generate a configuration?). All these can be unified under the rubric of mathematical logic. We will see how the tools of logic can address several of these problems in a somewhat uniform way.

    The talk will be self-contained, but does expect that the listener has a basic knowledge of logic (namely that the upside-down A is for-all and the backward E is there-exists).

  12. in Talks #2

    The Way of APL

    While early Von Neumann style programming gave way to Structured Imperative Programming, which in turn evolved into Functional and OOP programming paradigms that are currently very popular, another programming paradigm was maturing and developing: the array programming paradigm. This deeply misunderstood programming model receives equal parts derision and wonder, while remaining largely under-appreciated and under-utilized, despite numerous success stories as well as research and evidence to back up its sometimes miraculous claims. Modern computer designs and our need for better methods for dealing with the needs of rigor, correctness, performance, and scale warrants a deeper look into the subtleties that are embedded in the quintessential array programming language, APL.

  13. in Talks #1

    Designing Applications with Pluggable Layers Using Polymorphism

    The flagship product of IOHK is Cardano, the Proof-of-Stake (PoS) blockchain hosting the cryptocurrency Ada. Conceptually, the system can be divided into a stack of layers: the networking layer that distributes messages across the nodes, a cryptographic layer to handle signatures, a ledger layer that keeps track of funds and transactions, and in between, orchestrating everything, the consensus layer that implements the PoS protocol and determines how the nodes agree on a sequence of blocks.

    All of those layers are the subject of ongoing research and improvement, and we want to retain the ability to replace an individual layer, with minimal changes required on the rest of the system. In order to do that, we keep the consensus layer polymorphic in the types of the other layers. Replacing a layer then amounts to choosing another concrete instantiation.

    We show how to use Haskell’s type system to design such a polymorphic consensus layer. Features we use for that are Type Classes, Type Families, Phantom Types, and others.

  14. in Tutorials #2

    Type-Level Programming in Haskell

    How types help us solve real-world problems

    The Haskell type system is good for specifying user intentions and helping the compiler to check code correctness. Unfortunately, there is sometimes a barrier before that level where beginning Haskell programmer can read and write complex type annotations. This is often the case with such libraries as Lens or Servant. With this tutorial, I aim to bring participants behind that barrier. I’ll present several type-level programming tools including type families, GADTs, data kinds, and others all way down to ‘almost’ dependent types. Their description will be given together with practical examples as used in the modern Haskell libraries.

  15. in Tutorials #1

    Superficial SQL Indexing

    An Epidemic Plague

    What if a single root cause was responsible for most SQL performance issues?

    Proper indexing is a very time and cost-effective way to improve SQL performance. Yet hardly anyone gets it right so that about 50% of all SQL performance problems can be attributed to the index/query mismatch.

    In this tutorial I’ll explain how organisational structures hinder proper indexing and why it is not sufficiently covered in the relevant literature. Naturally, this tutorial will also explain how to approach indexing for a better result and demonstrate the most common indexing mistakes in a fun and educating way: in a live quiz with the audience.

  16. in Talks #2

    Analyzing Programs with SMT Solvers

    Have you ever wanted to prove non-trivial properties of your programs automatically? It’s actually practical with modern SMT solvers like Z3! I’ll walk you through how we can compile a program to an SMT formula and how we can use that formula to do bounded verification—checking assertions in our code statically or comparing a program against an executable specification. This technique is tricky in general purpose programming, but works wonders for domain-specific languages.

  17. in Talks #1

    Wire Once, Rewire Twice

    At Symbiont, we use a “modules-as-records-of-functions” to structure our services and share code. We need the ability to create components which can easily be wired together but also changed at will for unit or integration testing even if they are very far down in the dependency tree.

    This talk will show how we approached this problem, started solving it with 2 simple type classes but then came up with a much more simple way, relying on just one data structure!

    Not only this makes reconfiguring applications a breeze but the same technique can be applied to Hedgehog generators where you can define a “compositional language” to modify existing generators for nested data structures. You can now express things like “generate a model of shoe with only the colour blue and 2 sizes

  18. in Talks #2

    EventSourcing All Over the Place

    By now EventSourcing is an established alternative to handle and store data in the backend. But did you realize that frontend architecture patterns like Flux/Redux basically also work in an event-sourced way? Unfortunately, in these patterns the event store is inaccessible, though. With some simple tricks we can make use of it and establish proper EventSourcing in the frontend as well. Moreover, these events can also be used to synchronize changes in frontend and backend without the need to divert from the EventSourcing pattern.

    This talk demonstrates how this technique works in general and how it was used in a real project.

  19. in Talks #1

    Across Time and Space: Building Explorative UIs Using a Many-Worlds Interpretation of State

    The functional approach to state management in the frontend was first enabled by React, pioneered by the likes of om.next, Redux, and Elm, and has ushered in a golden era in web development. It is captured by the two signatures view :: DB -> HTML and mutate :: DB -> Tx -> DB. What might happen when we start working with more than one world, i.e. when we replace the notion of mutate with that of solve :: DB -> Tx -> [DB]? Using Clojure and Rust, we explore these ideas in the context of 3DF, a stream processing system based on differential dataflows.

  20. in Tutorials #1

    Einstieg in die Probabilistische Programmierung

    Die letzten Jahre hat Probabilistisches Programmieren Fahrt aufgenommen. Es wird mehr geforscht, publiziert, konferiert, entwickelt und auch angewendet.

    Der Einstieg ist durch die Integration in Mainstream-Sprachen wie Haskell, Scala und Python einfach geworden.

    Probabilistische Programme sind lernfähige Simulationen

    Kurz vorgestellt - alte Bekannte als Probabilistische Programme:

    • Naive Bayes
    • Markov-Kette
    • Bayes-Netze
    • Gauß-Prozesse

    Basics:

    • Eigenbau einer diskreten Wahrscheinlichkeitsmonade (Scala)
    • die Sampling-Variante von Rainier (Scala))
    • Olegs Freie Wahrscheinlichkeitsmonade (Haskell))

    Kurze Vorstellung der Algorithmen:

    • MCMC
    • Variational Bayesian Methods
    • Deep Probabilistic Programming: kann Tensorflow Probability wirklich mehr?

    Erfahrungsbericht - Probabilistische Logik für Fahrzeugkonfiguration:

    • Principle of Explosion: “ex falso quodlibet”
    • Markov-Logic mit Figaro (Scala)
  21. in Tutorials #2

    Writing Hardware in Haskell

    In this hands-on session, we will write Haskell programs, compile them into digital circuits, and flash them onto an FPGA (field programmable gate array).

    PGAs are computer chips containing logic and memory cells that can be dynamically reconfigured to implement various digital circuits. This allows to iteratively develop processors, highly parallel high-performance computations, networking stacks and more without having to manufacture a custom chip.

    While traditional hardware description languages (HDLs), exist to design these systems, circuit semantics are also nicely captured by purely functional programs. Clash in particular, can compile a subset of Haskell into traditional HDLs, providing powerful high-level abstractions and correctness guarantees. It also allows reusing large parts of the existing Haskell tooling and library ecosystem.

    We will start with an overview of digital circuits and FPGAs, explaining the flexibility and restrictions faced when designing hardware. After a quick demo of how to work with Clash, participants will write their own designs, test them in GHCi and compile them to hardware.

    The tutorial assumes basic proficiency with Haskell, including Functors and Applicatives. FPGAs and some additional hardware are provided, but a laptop is required to run Clash and an open source hardware design toolchain.

    Participants will

    • gain an understanding of the inner workings of digital circuits, which they are surrounded by in their daily lives
    • see examples of how to use types and common abstractions (Functor, …) to model properties of a domain
    • more generally experience the versatility and expressiveness of functional programming, inspiring them to solve problems in a multitude of domains outside of what they thought is possible.
  22. in Talks #1

    State machine modelling and property based testing combined with fault injection

    Property based tests of pure programs can give us great confidence that the involved functions are correct with regard to some specification. When the programs are monadic however, i.e. use the file system or the network for example, we need to be more careful because of exceptions.

    For example some file that the program uses might have the wrong permissions or some network traffic gets lost, causing our program to crash or lose data. The problem here is that typically when we run our tests none of these exceptions occur and the tests pass. Even a conscious effort to test for exceptions might be futile, because of the sheer amount of things that can possibly go wrong in a program (nevermind combinations of failures and dependencies on timing).

    In this talk I’ll show how we can overcome these testing difficulties by using state machine modelling and property based testing together with fault injection. Fault injection is a technique that purposely introduces faults into our system, for example network package loss.

    I gave a talk last year on combining property based testing and state machine specifications to test concurrent programs. In this years talk we’ll recall the basics and focus on exceptions rather than on concurrency, but of course nothing stops us from doing both.

  23. in Talks #2

    Emotional Programming

    We model the real world, we program behaviour, we build intelligent machines, we are creators of universes. Coders are mostly antisocial nerds. However, if you’re a non-nerd involved in a software project, you will need to deal with the code produced by the nerds, even if it’s as incomprehensible as their pick-up lines. Those incomprehensible programs, and the resulting mismatch between our minds, the world, and the code - are a key vulnerability of our universe. (And, if we continue to flood the real universe with IoT devices, that universe, too.) To address this vulnerability, people need to communicate - coders and non-coders, both about the code and through the code. We need code that is welcoming, empathic, charming, and beautiful. Software craftsmanship, functional programming, and domain-driven design all can help, but by themselves they are not enough. Mainusch and Sperber are cretins of communication: They can’t even decide which of them is the nerd. Sperber talks monads, Mainusch unsuccessfully waits for them to click. Mainusch talks ideas, Sperber puts code on slides. But in this talk, they will connect - and if they can connect, so can the people in your project. We walk a software lifecycle from back to front, giving examples for communication beauties and beasts alike, show how to overcome the inevitable communication breakdowns and find inspiration and beauty in your project.