raichoo

In this talk I will outline my journey implementing my X11 window manager hikari and the corresponding Wayland compositor shortly after. hikari is a stacking window manager/compositor with some tiling capabilities. It is still more or less work in progress and currently targets FreeBSD only but will be ported to Linux and other operating systems supporting Wayland once it has reached some degree of stability and feature completeness.

This talk covers:

• a brief explanation regarding differences between X and Wayland
• some of hikari's design goals and motivation
• choice of programming language
• an overview of libraries that were used
• tools for ensuring code quality and robustness
• obstacles
• resources that helped me to implement the whole thing

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.

DTrace is an incredibly useful tool for safely inspecting whole systems without impacting overall performance as much as other mechanisms. It's open source and available on a wide variety of operating systems like FreeBSD, MacOS, Solaris, illumos and NetBSD. It can be used for debugging, reverse engineering or for just learning to understand the system. I'm going to introduce DTrace and its D language by digging down into the inner workings of FreeBSD itself as it runs (e.g. memory and process management, locking infrastructure and scheduling) as well as user processes. On top of that I will use DTrace itself to illustrate how DTrace is doing its work. We are also going to take a look at some of DTraces' internals like some of the design decisions as well as the byte code that is being executed in the kernel.

Idris is a relatively young research programming languages that attempts to bring dependent types to general purpose programming. In this talk I will introduce the concept of dependent types and the Curry-Howard isomorphism and how these can be applied to prove properties about software and eradicate whole classes of bugs and security issues.

Building robust software is a hard task these days. As software gets more complex it gets increasingly hard to reason about it, this leads to a larger attack surface for bugs and security flaws. Some of these bugs can be completely eliminated with the introduction of type systems that keep our values at runtime in check. Type systems are in fact the most widespread mechanism to verify correctness properties of programs, with dependent types we take this to the next level. While most dependently typed systems (e.g. Coq and Agda) aim to be proof assistants rather than programming languages. Idris tries to answer the question how a general purpose programming language with dependent types could look like, it also enables us to produce self contained binaries as well as JavaScript applications today. In this talk I will introduce techniques for programming with dependent types as well as interaction with the programming language itself. Examples will present resource tracking in the type system e.g. tracking file handles and yielding compilation errors on resource leaks, modeling specifications of protocols as types and enforcing them. I argue that functional programming and dependently typed programming languages provide various exciting opportunities to the programmer, including a powerful mental model, compositionality and machine assisted programming through interactive editing capabilities. The presentation software for this talk will be a web application written in Idris which compiles to JavaScript using a compiler backend written by the lecturer.