Writing, Articles, Podcasts

TypeScript – Die Komplexität von JavaScript bändigen

2022 feiert TypeScript zehnjähriges Jubiläum. Anlass genug, auf die Anfänge zurückzublicken – und Einsteigern alles an die Hand zu geben, was sie für die Arbeit mit der Programmiersprache brauchen.

Veröffentlicht in t3n 66 am .

Was macht eigentlich ein Bundler?

In der Frontend-Entwicklung kommt man selten ohne JavaScript aus. Gestandene Backend-Profis sehen sich dann mit einer komplett neuen Toolchain konfrontiert, die vor unbekannten Fachbegriffen nur so strotzt. Doch hinter der Komplexität steckt System.

Veröffentlicht in Informatik Aktuell am .

#SoftwareArchitektur – Funktionale Programmierung in der Praxis

Keine Seiteneffekte, einfaches Testen, die Korrektheit der Programme kann sogar bewiesen werden - alles Vorteile von funktionaler Programmierung. Sie hat im akademischen Bereich schon immer eine Rolle gespielt, aber auch in der Industrie wird sie zunehmend populärer - aber gleichzeitig wirkt sie abgehoben und schwer zu verstehen. In dieser Episode berichten Lars Hupel und Isabel Wingen darüber, wie sie von funktionaler Programmierung im Projekt-Alltag profitieren, welche Erfahrungen sie gemacht haben und wie man selber starten kann.

Veröffentlicht in Softwarearchitektur im Stream am .

How to build your own personal DynDNS service

Consumer-grade internet subscriptions typically come with NAT and dynamically-assigned IP addresses. In order to reach my home server from the outside, I decided to build my own dynamic DNS service. The reason was twofold: I found the existing providers I had used in the past to be annoying. I wanted...
Published on .

Injecting environment variables into static websites using NGINX

Static site generation is a perfect fit for publishing documentation. In a recent project, we chose to use NGINX as a web server to host the HTML and CSS files. However, we also wanted to protect the site using SSO. This is where things get a bit difficult.

Published in INNOQ on .

Countries I've been to

Map of Europe

I thought it’d be fun to collect a list of all countries I’ve been to. This list will be updated every time I visit a new one.

Published on . Image credits: TheAndrasBarta.

Hiking in Slovakia

Ďumbier mountain
Last month I went on a hiking vacation. Planning started out by wanting to visit a friend in Hungary, but because of Covid, it did not seem wise to visit Budapest and go to museums or other indoor activities (although all of us are vaccinated). So I browsed a map...
Published on . Image credits: Jerzy Opioła (CC-BY-SA 4.0).

Warum die Briefwahl nur die zweite Wahl sein sollte

In zwei Wochen ist Bundestagswahl. Es ist zu erwarten, dass der Anteil der Briefwähler:innen weiterhin ansteigen wird. Nach Medienberichten rechnet die Deutsche Post mit mindestens 40 %, trifft aber auch Vorbereitungen für 60 %. Dieser Trend zeichnet sich bereits seit längerer Zeit ab: bei der vergangenen Bundestagswahl 2017 nahmen in...
Veröffentlicht am .

Proof of Stake. Wie hoch ist dein Einsatz?

Cardano tut es bereits und Ethereum will es tun: Immer mehr Kryptowährungen nutzen „Proof of Stake“ als Alternative zum etablierten „Proof of Work“-Konzept, wenn es um die Absicherung ihrer Blockchain geht. Warum tun sie das? Und wo liegen die Vor- und Nachteile? Darüber sprechen Lucas und Lars in dieser Folge. Außerdem werfen sie einen Blick über den Tellerrand und geben einen Überblick über weitere Methoden, mit denen Blockchains vor Manipulation geschützt werden können.

Veröffentlicht in INNOQ-Podcast am .

Benutzerfreundlicher Äther: Smart Contracts in dezentrale Applikationen einbetten

Smart Contracts, wie sie die Ethereum-Blockchain kennt, sind technisch eine feine Sache. Aber sie brauchen eine Bedienoberfläche, wenn sie nicht nur Entwicklern nützen sollen – dann werden daraus „dezentrale Applikationen“. Um so eine DApp zu programmieren braucht man nur etwas HTML und JavaScript.

Veröffentlicht in c't am .

Geld statt Kohle: Warum Kryptowährungen auf Proof of Stake umstellen wollen

Viele Kryptowährungen nutzen Blockchains mit „Proof of Work“, aus dem ein enormer Energieverbrauch resultieren kann. „Proof of Stake“ löst dieses Problem, doch das Verfahren hat auch Nachteile. Ganz ohne Proof of Irgendwas lässt sich eine Kryptowährung aber kaum realisieren.

Veröffentlicht in c't am .

A hiatus from Open Source

About ten years ago – in 2011 – I opened my first pull request to a major Scala open source project.1 At the time, I was still a Bachelor’s student in Computer Science. The contribution was part of a course that was offered by the Didactics unit in our CS...
Published on .

Decentralized Architecture: What’s Behind Blockchains?

Fueled by ever new highs in cryptocurrency prices, there is currently a lively debate about blockchains. Some praise the “self-sustaining” currencies as saviors in times of crisis, while others see their excessive power consumption as a climate killer. But which opportunities and risks the new technologies harbor for software architecture is rarely a matter of debate. I would like to give a brief overview of this issue.

Published in iSAQB on .

Dezentralisierte Architektur: Was steckt hinter Blockchains?

Befeuert von immer neuen Kurshöhen der Kryptowährungen, findet derzeit eine lebhafte Debatte über Blockchains statt. Die einen preisen die „autarken“ Währungen als Heilsbringer in Krisenzeiten, die anderen sehen im exzessiven Stromverbrauch einen Klimakiller. Doch welche Chancen und Risiken die neuen Technologien für Softwarearchitektur bringen, wird selten diskutiert. Über diese Fragestellung möchte ich hier einen kleinen Überblick geben.

Veröffentlicht in iSAQB am .

Die Top 5 der Neuerungen in Scala 3

Red stairway

Schon seit geraumer Zeit arbeitet das Team um Martin Odersky an der nächsten großen Version von Scala. Deren Spitzname „Dotty“ leitet sich ab von „Dependent Object Types“, dem logischen Kalkül, welches dem Typsystem zugrunde liegt. Doch es gibt nicht nur Verbesserungen in den Eingeweiden des Compilers. Die aktuell in der Release-Candidate-Phase befindliche Vorschau auf Scala 3 verspricht, das Programmiererlebnis deutlich zu verbessern.

Veröffentlicht in Javamagazin 07/2021 am . Bildnachweis: stokpic/Pixabay.

Den Äther programmieren: Smart Contracts für die Ethereum-Blockchain schreiben

Bei Ethereum denken viele an eine Kryptowährung, dabei handelt es sich eigentlich um ein weltweit verteiltes Rechenzentrum, das Programme – sogenannte Smart Contracts – auf einer Blockchain ausführt. Wir zeigen Ihnen, wie Sie einen solchen Smart Contract programmieren, um „Schere, Stein, Papier“ auf der Ethereum-Blockchain zu spielen.

Veröffentlicht in c't am .

Geld im Äther: Ein kleiner Praxisleitfaden zu Ethereum-Wallets

Tesla akzeptiert Bitcoin-Zahlungen, auf Ethereum werden Tweets verkauft – von Kryptowährungen hört man ständig. Aber wie benutzt man so ein System, wie kommt man an das virtuelle Geld und wie überweist man es? Zum entspannten Lernen eignet sich Ethereum: Dessen Blockchain ist einfach zu benutzen und erlaubt freies Experimentieren in Testnetzen.

Veröffentlicht in c't am .

Verträge im Äther: Eine Einführung in die Ethereum-Blockchain

Blockchains werden oft mit Kryptowährungen gleich­gesetzt, aber die Technologie kann mehr als Geld verwalten. „Smart Contracts“ erlauben die Blockchain als Computer zu ­benutzen und ermöglichen zum Beispiel virtuelle Organi­sationen oder Non-Fungible-­Tokens (NFT). Ethereum ist der Vorreiter bei diesen Anwendungen.

Veröffentlicht in c't am .

Fahrradstrecken in & um München

Auf dieser Seite sammle ich Beschreibungen für Tages- oder Halbtagestouren in & um München. Alle Strecken bin ich selbst gefahren.

Veröffentlicht am .

Why is it so hard to reuse formally verified code?

Log starts at March 15, 2021, 7:51 PM CET. Slightly edited for improved legibility. Hillel, 7:51: So Lars and I want to try something new: a COLLABORATIVE tweetstorm. The topic? Why it’s so hard to reuse formally verified code. They’re an expert in verifying code with Isabelle, I use TLA+....
Published on .

Routing the technical interview

Blue and red boat on sea under white clouds during daytime
“Welcome, Nephele!” he said. The interviewer couldn’t help but notice her name, Nephele. It sounds Greek. But he didn’t ask, not wanting to get off on the wrong foot with the promising candidate. He made a mental note to look up the name afterwards. “I believe HR already told you...
Published on . Image credits: Andrey Sharpilo.

My local DNS setup

A few years ago, I wrote about the hardware setup of my home server. Recently, I’ve decided to put it to work beyond storing mere data and mirroring my IMAP server. I was annoyed by the weird behaviour of local name resolution of my home router, so why not operate...
Published on .

Smart Contracts programmieren in Ethereum – Gegenwart & Zukunft

Ethereum steht hinter einer der populärsten Kryptowährungen – und doch ist es noch sehr viel mehr. Damit kann kryptografisches Geld dank Algorithmen nämlich völlig autonom verwaltet werden. Aber wie funktionieren die sogenannten Smart Contracts und wo geht die Reise hin?

Veröffentlicht in t3n 63 am .

Conferences I've been to

Map of Europe

I thought it’d be fun to collect a list of all conferences I’ve been to. There were a lot of them; at least fifty it seems. Maybe we’ve even crossed paths somewhere.

Published on . Image credits: TheAndrasBarta.

#SoftwareArchitektur – Diversity

Gerade in der Software-Entwicklung sind viele Gruppen unterrepräsentiert. Führen zu homogene Teams eigentlich zu schlechterer Software? Und warum? Das Thema hat auf jeden Fall Auswirkungen auf Software-Architekt:innen, unser Arbeitsumfeld und unsere Arbeitgeber. In dieser Episode diskutieren wir mit Lars Hupel, Lena Kraaz und Aminata Sidibe von INNOQ, wie Diversity in der Software-Architektur und -Entwicklung verbessert werden kann und ob das eine gute Idee ist.

Veröffentlicht in Softwarearchitektur im Stream am .

Stufe 3: Neuerungen in der dritten Version der Programmiersprache Scala

Red stairway

14 Jahre nach Erscheinen von Scala 2.0 wagt die Sprache den nächsten großen Schritt. Wird Scala mit Version 3 so, wie es immer sein sollte? Ein Release Candidate steht schon in den Startlöchern und zeigt, wie sich die Scalable Language weiterentwickelt.

Veröffentlicht in c't am . Bildnachweis: stokpic/Pixabay.

Deploying a WebAssembly smart contract on Oasis Ethereum

One of the cornerstones of Ethereum 2.0 is the migration from the “classic” EVM to a WebAssembly-based virtual machine. In this post, I explain how to deploy a compiled WebAssembly contract to the Oasis Ethereum chain.

Published in INNOQ on .

Jahresend-Mix 2020

Welche Security-Themen haben euch 2020 am meisten beschäftigt? Was hat euch besonders beeindruckt oder einfach nur überrascht? Diese Fragen stellte Simon Kölsch 16 INNOQ Kolleginnen und Kollegen. Die Antworten ergeben einen bunten Themen-Mix, angefangen mit der Bedeutung von UX in der Security über Threat Modelling bis hin zu neuen Ideen für die spielerische Auseinandersetzung mit Security-Themen.

Veröffentlicht in INNOQ-Security-Podcast am .

Informatik-Theorie für praktizierende Architekten

In dieser Episode des SoftwareArchitekTOUR-Podcasts spricht Stefan Tilkov mit Gast Lars Hupel über den Nutzen von Informatik-Grundlagenwissen für praktizierende Softwarearchitekten.

Veröffentlicht in SoftwareArchitektTOUR am .

Dependently-Typed TypeScript

TypeScript ist eine Programmiersprache mit einigen Besonderheiten: Im Gegensatz zu den allermeisten anderen getypten Programmiersprachen wurde sie als Aufsatz für JavaScript (JS) entwickelt. Dabei hat Microsoft besonderen Wert darauf gelegt, dass sich die Sprache möglichst nahtlos in die bestehenden Ökosysteme (Node.js und Browser) integriert. Das wird dadurch erreicht, dass die TypeScript-Syntax „bloß“ die Typen zu JavaScript hinzufügt und die Kompilierung aus dem Entfernen der Typannotationen besteht. Damit hat sich TypeScript zum de-facto Standard entwickelt, wenn es darum geht, typsichere Anwendungen auf JS-Basis zu bauen.

Veröffentlicht in Funktionale Programmierung am .

Postel’s Law. Grob gehackt oder fein geschnitten?

Grob gehackt oder lieber ein feiner Julienne-Schnitt für die Tags in der Suppe? Lucas und Lars diskutieren in dieser Folge über Postel’s Law. Was es besagt und wie liberal ein Service eigentlich beim Akzeptieren von Eingabedaten sein sollte – darum geht’s in dieser Folge!

Veröffentlicht in INNOQ-Podcast am .

Smart Contracts in der Programmiersprache Rust

Wie wäre es, Rust in Kombination mit WebAssembly zu nutzen, um Smart Contracts zu entwickeln, die gegebenenfalls Millionen von Krypto-Tokens verwalten können?

Veröffentlicht in Heise Developer am .

Train Consists

Poor Lars is having trouble arranging cars in his trains. Annie helps him out using constraint programming.

Published in Playing with Prolog (Season 3) on .

Modernes funktionales Programmieren in Java

Erfahrene Java-Entwickler*innen können viele der Entwurfsmuster des „Gang of Four“-Buches aus dem Stand zitieren, identifizieren und anwenden. Trotzdem stehen diese praktisch seit der Erscheinung des Buches unter Kritik: da sie teils vage definiert sind, strotzen „moderne“ Codebasen nur so von Singletons, Factories und Buildern. Auf der anderen Seite stehen die Anhänger*innen der funktionalen Programmierung, die sich gerne über die objektorientierten Patterns lustig machen. Die Wahrheit liegt wie so oft in der Mitte: seit Version 8 lassen sich auch in Java die cleveren Gedanken aus der funktionalen Welt effektiv und komfortabel benutzen, ohne die Objektorientierung aufzugeben.

Veröffentlicht in JavaSPEKTRUM 4/2020 am .

An introduction to Conflict-Free Replicated Data Types

This is a series about Conflict-Free Replicated Data Types, or CRDTs for short. Their purpose is to allow seamless replication of data on different nodes in a distributed system. Merging is by construction always possible, without any conflicts. This series assumes no knowledge about CRDTs, but be prepared to learn a thing or two about algebras.

Published on .

TypeScript. Was sind das denn für Typen?

TypeScript ist in aller Munde. In dieser Folge will Lucas von Lars wissen, wieso er sich so sehr für diese Sprache begeistert. Wie ordnet ein erfahrener Scala-Entwickler wie Lars das Typsystem von TypeScript ein? Lars beschreibt zudem, welche Vorteile ein mächtiges Typsystem mit sich bringt, und erklärt, wie die Interaktion mit JavaScript-Bibliotheken funktioniert.

Veröffentlicht in INNOQ-Podcast am .

Remote Training, funktioniert das?

Heimarbeit hat sich mittlerweile – mehr oder weniger freiwillig – bei den meisten Unternehmen in der IT durchgesetzt. Doch beim Thema Schulungen sind viele noch skeptisch, ob das funktionieren könnte. Wir haben es für das iSAQB-Modul BLOCKCHAIN ausprobiert.

Veröffentlicht in INNOQ am .

Cross-platform testing of TypeScript code with Jasmine and Karma

I like TypeScript. Writing code that already underwent basic checks (i.e. typechecking) before it can even touch an execution engine is a big win in my book. In particular, TypeScript is nice because it integrates well into the broader JavaScript ecosystem and comes with batteries (i.e. types) included. Unfortunately, most test runners require extra setup to work with tests written in TypeScript. Some even require staggering amounts of configuration.

Published in INNOQ on .

Lars Hupel on Algebraic Design

In this episode of the CaSE podcast, Lucas talks to Lars Hupel of Typelevel-fame about algebraic design. Lars starts to explain how the expression problem views the difference between the functional and Object Oriented style of programming. He then explains the concept of an algebra – from coupling trains to CRDTs. This leads to a discussion on comprehensive and iterative thinking styles and how different styles of testing and proving work. Finally, they bring it all back to type systems.

Published in CaSE podcast on .

So you want to compose some functions

Let’s say you have a list of functions and you want to compose them. Shouldn’t be too hard, right? Of course it is, but maybe there’s an elegant way.

Published in INNOQ on .

2019 in Review

2019 was a remarkable year for me: a year of many firsts. From starting a job in industry to finishing my PhD, I want to review what happened this year. Let’s start with my professional life. At some point mid-2018, my advisor asked me about how I felt about becoming...
Published on .

Das eierlegende Truffleschwein

Historisches Bild eines Trüffelschweins

Viele, die im Java-Umfeld unterwegs sind, werden von ihr gehört haben: der sagenumwobenen GraalVM. Diese magische neue Virtual Machine für Java soll vor allem für blanke Performance sorgen, indem sie den Java-Bytecode in nativen Code kompiliert. Dadurch fällt insbesondere der Startup-Overhead weg, da weite Teile der Initialisierung bereits vom Compiler erledigt werden. So oder so ähnlich ist es vielerorts zu lesen. Hinzu kommt, dass die GraalVM zu nicht weniger das Potential hat als eine neue Ära der polyglotten Programmierung auf der JVM einzuläuten. Die Rede ist von der Truffle API, einem generischen Framework zur Implementierung von Interpretern.

Veröffentlicht in Javamagazin 01/2020 am . Bildnachweis: gemeinfrei.

A week in Tokyo

Hydrangea in Kamakura
I’m not regularly in the habit of writing personal blog posts. I had an old blog once in which I shared my experiences during my Erasmus semester in Northern Ireland. After that, I have largely resorted to technical writing. This text is an attempt to balance that out again; mostly...
Published on . Image credits: me.

Verified Code Generation

This page contains the archived research information relating to the paper “A Verified Compiler from Isabelle/HOL to CakeML”. It reflects the state from approximately October 2019. For a list of all publications, refer to this page. Goal Development of a verified code generator from Isabelle/HOL to CakeML, a verified subset...
Published on .

Falsehoods Programmers Believe About Gender

Gender select form with options: Male, Female, Custom (upload custom gender, max 10 MB)
Are you storing gender in your database? Are you having trouble with those annoying queers being annoying about it? Chances are you’re the annoying one. But don’t worry, this list will clear up some common misunderstandings. There are only two genders. Okay, maybe not. But there are only two biological...
Published on . Image credits: @chordbug.

The many ways of testing Smart Contracts in Ethereum

You have implemented a smart contract for Ethereum, and now you are wondering how you can test it under real-life conditions, but without spending money in case there’s a problem? Luckily, there are test networks that can help you with this.

Published in INNOQ on .

Private Blockchains: Vergleich von Fabric und Corda

Der Markt an Blockchain-Technologien ist hart umkämpft. Seit der Einführung von Bitcoin kam es zu einer Proliferation von Forks, Neuentwicklungen und Innovationen. Doch im Unternehmenskontext ist es selten sinnvoll, interne Geschäftsvorgänge auf öffentlichen Blockchains zu verwalten. Daher etabliert sich im Moment eine neue Nische, die der privaten oder zugangsbeschränkten (permissioned) Blockchains.

Veröffentlicht in JavaSPEKTRUM 5/2019 am .

Tabling

We cover the newly added Tabling for SWI-Prolog to help Annie get around Bangalore.

Published in Playing with Prolog (Season 3) on .

Integrating Logback with JLine

Logback is a popular logging library for Java. JLine can be used to create nice shell-like applications. Combining both is not as hard as it looks.

Published in INNOQ on .

Verification of smart contracts

A moth on a piece of paper, believed to be the first computer bug

Smart contracts are used to execute code on blockchains. A variety of business cases are now represented with such contracts. Ethereum is a popular platform for this purpose. However, as with all software, the question arises of how to ensure the quality of the code.

Published in INNOQ on . Image credits: U.S. Naval Historical Center.

Verifikation von Smart Contracts

A moth on a piece of paper, believed to be the first computer bug

Smart Contracts sind eine Technologie, mit der man Code auf Blockchains ausführt. Eine Vielzahl von Geschäftsfällen werden inzwischen durch solche Verträge abgebildet. Ethereum ist dafür eine beliebte Plattform. Doch wie bei aller Software stellt sich die Frage, wie man die Qualität des Codes sicherstellen kann.

Veröffentlicht in INNOQ am . Bildnachweis: U.S. Naval Historical Center.

Scala Days 2019 in Lausanne

Im Juni 2019 fanden die Scala Days anlässlich des 10. Jubiläums wieder in Lausanne – an der Geburtsstätte von Scala – statt. Heuer gab es nicht nur zwei Konferenztage, sondern auch eine ganze Reihe von Community-Events davor und danach. INNOQ war die ganze Woche vor Ort und unsere Kollegen berichten hier von ihren Erfahrungen.

Veröffentlicht in INNOQ am .

Adressen und Transaktionen in Kryptowährungen – Teil 3: Altcoins

Kryptowährungen sind in aller Munde. Tutorials und Erklärungen gibt es zuhauf. In dieser Artikelserie soll ein bestimmter Aspekt, nämlich der der Adressen und Transaktionen, detailliert für populäre Blockchains geklärt werden. Denn unter der Oberfläche verbirgt sich einiges an Komplexität. Teil 3: Altcoins.

Veröffentlicht in INNOQ am .

Parametrizität in Java

So gut wie alle modernen Programmiersprachen erlauben es, Routinen über Werte und über Typen zu parametrisieren. In Java wird letzteres „Generics“ genannt, in C++ hingegen „Templates“. Obwohl die Konzepte die gleichen sind, unterscheidet sich die Implementation doch stark. In diesem Artikel möchte ich diese Art der Parametrisierung in Java unter die Lupe nehmen und erklären, warum „Type Erasure“ doch eine ganz gute Idee ist.

Veröffentlicht in JavaSPEKTRUM 3/2019 am .

Adressen und Transaktionen in Kryptowährungen – Teil 2: Ethereum

Kryptowährungen sind in aller Munde. Tutorials und Erklärungen gibt es zuhauf. In dieser Artikelserie soll ein bestimmter Aspekt, nämlich der der Adressen und Transaktionen, detailliert für populäre Blockchains geklärt werden. Denn unter der Oberfläche verbirgt sich einiges an Komplexität. Teil 2: Ethereum.

Veröffentlicht in INNOQ am .

Adressen und Transaktionen in Kryptowährungen – Teil 1: Bitcoin

Kryptowährungen sind in aller Munde. Tutorials und Erklärungen gibt es zuhauf. In dieser Artikelserie soll ein bestimmter Aspekt, nämlich der der Adressen und Transaktionen, detailliert für populäre Blockchains geklärt werden. Denn unter der Oberfläche verbirgt sich einiges an Komplexität. Teil 1: Bitcoin.

Veröffentlicht in INNOQ am .

Node-RED

IBM’s node-red flow programming language is an interesting declarative language. Recently Annie’s been experimenting with it. In this video she shows it to Lars.

Published in Playing with Prolog (Season 2) on .

Job Scheduling

This month in Playing with Prolog we help Lars out at work. He needs to schedule jobs for his CI servers.

Published in Playing with Prolog (Season 2) on .

Marelle

Playing with Prolog is back for Season 2 with a new host. Annie and Lars take a look at Marelle, the SWI-Prolog based devops system.

Published in Playing with Prolog (Season 2) on .

My storage server setup

Updated continuously after publication. Recently I announced on Twitter some upgrade I did on a “home” server: Successfully upgraded the home server from 9 TB to 15 TB storage. A dozen devices all want to be backed up. Lars Shortly thereafter, someone wanted to know what the setup looks like....
Published on .

Let's build ourselves a small ScalaCheck

ScalaCheck is a well-known property-based testing library, based on ideas from Haskell’s QuickCheck. It is also a Typelevel project. In this post, I’d like to show some of the underlying mechanisms, stripped down to the bare minimum.

Published in Typelevel.org blog on .

Functional Geekery, Episode 62

In this episode Proctor talks with Lars Hupel. We talk his introduction to Functional Programming with Haskell, Scala, and move to working on Isabelle for creating theorems about proving your program.

Published in Functional Geekery on .

Formale Wahrheit

Am Lehrstuhl für Logik und Verifikation der TUM wird Isabelle entwickelt, ein Programm mithilfe dessen man Theoreme beweisen kann. Interaktive Theorembeweiser sind relative neue Hilfsmittel in der Werkzeugsammlung von Mathematikern. Sind solche vom Computer verifizierten Argumentationsketten aber noch Beweise im mathematischen Sinn?

Veröffentlicht in fatum am .

Ein Semester in Belfast

Dieser Artikel enthält gesammelte Texte aus meinem Blog aus der Zeit vom September 2010 bis zum Januar 2011, während der ich ein Austauschsemester an der Queen’s University of Belfast absolvierte. In meinem Blog habe ich für Familie, Freunde und Bekannte meine Eindrücke und Erfahrungen festgehalten. Zur gleichen Zeit studierte auch noch ein Münchner Kommilitone in Belfast, ein weiterer in Newcastle und ein Freund aus Heidelberg in Durham. Von jenen wird im folgenden auch das ein oder andere Mal die Rede sein. Die Texte sind hier nicht in ihrer chronologischen Reihenfolge wiedergegeben, sondern thematisch gruppiert. Insofern habe ich einige kleine Änderungen vorgenommen, um logische Sprünge zu vermeiden.

Veröffentlicht am .

Law Enforcement using Discipline

Some nine or ten months ago, Spire’s project structure underwent a major reorganization. Simultaneously, the Scalacheck bindings were refactored, completely overhauling the law-checking infrastructure.

Published in Typelevel.org blog on .

Deriving Type Class Instances

The use of type classes has become pervasive in Scala programming. Type classes are encoded as traits, hence the most basic way of declaring an instance is writing implicit methods which return objects extending from these traits. However, those implicit methods are regular Scala methods, so we can use all features provided by the language to derive instances. In this post, a technique is described to compose instances into larger ones, which will not only allow for construction of instances for case classes, but also for other nested structures with minimum boilerplate.

Published in Typelevel.org blog on .

Geschichtsrevisionismus

Was unter Historikern verpönt ist, ist mit Git ganz einfach: Die Geschichte eines Projekts im Nachhinein ändern. Welche Möglichkeiten es da gibt, soll in diesem Artikel kurz vorgestellt werden. (Dieser Artikel erschien ursprünglich im KaffeeKlatsch 09/2011.)

Veröffentlicht am .

Überholt

In der letzten Ausgabe des KaffeeKlatsch wurde eine Kombination aus Subversion, Mantis und CheckStyle vorgestellt. Dem ein oder anderen Leser beschlich beim Lesen des Wortes Subversion vielleicht ein seltsames Gefühl: Schreiben wir nicht das Jahr 2010? Der folgende Artikel hat sich zum Ziel gesetzt, die gängigen Vorbehalte gegenüber moderneren Tools zu zerstreuen und eine Umstellung, weg von Subversion, zu motivieren. (Dieser Artikel erschien ursprünglich im KaffeeKlatsch 09/2010.)

Veröffentlicht am .

Analysis für Informatiker

Inoffizielles Skript zur Vorlesung „Analysis für Informatiker“ des WS 2009/2010, gehalten von Prof. Dr. P. Rentrop, niedergeschrieben und illustriert von Markus Grimm, Andreas Heider, Lars Hupel, Michael Kerscher, Philipp Meyer, Janosch Peters und Sylvester Tremmel.

Veröffentlicht am .

Javastars

v.l.n.r.: ich, Richard Tschirschnitz, Thomas Milde

Wir, Lars Hupel, Thomas Milde und Richard Tschirschnitz sowie unserer Lehrer Mirko König sind am 5. Mai 2007 nach San Francisco geflogen, um an der weltweit größten Entwicklerkonferenz – der JavaOne 2007 – teilzunehmen. Dies hatten wir als 1. Preis beim Programmierwettbewerb „Java Stars 2006 – Sun Microsystems Award“ gewonnen und durften daher für einige Tage in den USA verweilen.

Veröffentlicht am . Bildnachweis: MK.