Joachim Breitner

Blog

Farewall green cap

Published 2017-05-05 in sections English.

For the last two years, I was known among swing dancers for my green flat cap:

Monti, a better model than me

Monti, a better model than me

This cap was very special: It was a gift from a good friend who sewed it by hand from what used to be a table cloth of my deceased granny, and it has traveled with me to many corners of the world.

Just like last week, when I was in Paris where I attended the Charleston class of Romuald and Laura on Saturday (April 29). The following Tuesday I went to a Swing Social and wanted to put on the hat, and noticed that it was gone. The next day I bugged the manager and the caretaker of the venue of the class (Salles Sainte-Roche), and it seems that the hat was still there, that morning, im Salle Kurtz1, but when I went there it was gone.

And that is sad.

The last picture with the hat

The last picture with the hat


  1. How fitting, given that my granny’s maiden name is Kurz.

Mütze Ade

Published 2017-05-04 in sections Deutsch.

Seit wohl etwa zwei Jahren ist eine grüne Mütze mein Markenzeichen beim Swing-Tanzen:

Monti, das bessere Model

Monti, das bessere Model

Diese Mütze war etwas besonderes, denn sie war ein Geschenk von einer guten Freundin, handgenäht aus einem Tischtuchstoff meiner verstorbenen Oma, und reiste mit mir schon in viele Ecken der Welt.

So auch letzte Woche nach Paris, wo ich am Samstag bei Romuald und Laura einen Charleston-Kurs besuchte – und als ich dann am Dienstag beim Social in Le Chalet du Parc die Mütze aufziehen wollte, war sie nicht mehr da. Ich habe zwar noch den Verwalter und den Hausmeister der Salles Saite-Roche, dem Veranstaltungsort des Kurses, aufgescheucht, und die Mütze wurde wohl noch am Vormittag im Salle Kurtz1 gesehen, aber ich war zu spät und die Mütze ist nun weg.

Und das ist schade.

Das letzte Bild mit Mütze

Das letzte Bild mit Mütze


  1. Wie passend, meine Oma ist eine geborene Kurz.

ghc-proofs rules more now

Published 2017-04-27 in sections English, Haskell.

A few weeks ago I blogged about an experiment of mine, where I proved equalities of Haskell programs by (ab)using the GHC simplifier. For more details, please see that post, or the video of my talk at the Zürich Haskell User Group, but one reason why this approach has any chance of being useful is the compiler’s support for rewrite rules.

Rewrite rules are program equations that the programmer specifies in the source file, and which the compiler then applies, from left to right, whenever some intermediate code matches the left-hand side of the equation. One such rule, for example, is

{-# RULES "foldr/nil" forall k z. foldr k z [] = z #-}

taken right out of the standard library.

In my blog post I went through the algebraic laws that a small library of mine, successors, should fulfill, and sure enough, once I got to more interesting proofs, they would not go through just like that. At that point I had to add additional rules to the file I was editing, which helped the compiler to finish the proofs. Some of these rules were simple like

{-# RULES "mapFB/id" forall c. mapFB c (\x -> x) = c #-}
{-# RULES "foldr/nil" forall k n. GHC.Base.foldr k n [] = n #-}
{-# RULES "foldr/undo" forall xs. GHC.Base.foldr (:) [] xs = xs #-}

and some are more intricate like

{-# RULES "foldr/mapFB" forall c f g n1 n2 xs.
    GHC.Base.foldr (mapFB c f) n1 (GHC.Base.foldr (mapFB (:) g) n2 xs)
    = GHC.Base.foldr (mapFB c (f.g)) (GHC.Base.foldr (mapFB c f) n1 n2) xs
    #-}

But there is something fishy going on here: The foldr/nil rule is identical to a rule in the standard library! I should not have to add to my file that as I am proving things. So I knew that the GHC plugin, which I wrote to do these proofs, was doing something wrong, but I did not investigate for a while.

I returned to this problem recetly, and with the efficient and quick help of Simon Peyton Jones, I learned what I was doing wrong.1 After fixing it, I could remove all the simple rules from the files with my proofs. And to my surprise, I could remove the intricate rule as well!

So with this bug fixed, ghc-proofs is able to prove all the Functor, Applicative and Monad rules of the Succs functor without any additional rewrite rules, as you can see in the example file! (I still have to strategically place seqs in a few places.)

That’s great, isn’t it! Yeah, sure. But having to introduce the rules at that point provided a very good narrative in my talk, so when I will give a similar talk next week in Pairs (actually, twice, first at the university and then at the Paris Haskell meetup, I will have to come up with a different example that calls for additional rewrite rules.

In related news: Since the last blog post, ghc-proofs learned to interpret proof specifications like

applicative_law4 :: Succs (a -> b) -> a -> Proof
applicative_law4 u y = u <*> pure y
                   === pure ($ y) <*> u

where it previously only understood

applicative_law4 = (\ u (y::a) -> u <*> (pure y :: Succs a))
               === (\ u (y::a) -> pure ($ y) <*> u)

I am not sur if this should be uploaded to Hackage, but I invite you to play around with the GitHub version of ghc-proofs.


  1. In short: I did not initialize the simplifier with the right InScopeSet, so RULES about functions defined in the current module were not always applied, and I did not feed the eps_rules to the simplifier, which contains all the rules found in imported packages, such as base.

veggies: Haskell code generation from scratch

Published 2017-04-21 in sections English, Haskell.

How hard it is to write a compiler for Haskell Core? Not too hard, actually!

I wish we had a formally verified compiler for Haskell, or at least for GHC’s intermediate language Core. Now formalizing that part of GHC itself seems to be far out of reach, with the many phases the code goes through (Core to STG to CMM to Assembly or LLVM) and optimizations happening at all of these phases and the many complicated details to the highly tuned GHC runtime (pointer tagging, support for concurrency and garbage collection).

Introducing Veggies

So to make that goal of a formally verified compiler more feasible, I set out and implemented code generation from GHC’s intermediate language Core to LLVM IR, with simplicity as the main design driving factor.

You can find the result in the GitHub repository of veggies (the name derives from “verifiable GHC”). If you clone that and run ./boot.sh some-directory, you will find that you can use the program some-directory/bin/veggies just like like you would use ghc. It comes with the full base library, so your favorite variant of HelloWorld might just compile and run.

As of now, the code generation handles all the Core constructs (which is easy when you simply ignore all the types). It supports a good number of primitive operations, including pointers and arrays – I implement these as need – and has support for FFI calls into C.

Why you don't want to use Veggies

Since the code generator was written with simplicity in mind, performance of the resulting code is abysmal: Everything is boxed, i.e. represented as pointer to some heap-allocated data, including “unboxed” integer values and “unboxed” tuples. This is very uniform and simplifies the code, but it is also slow, and because there is no garbage collection (and probably never will be for this project), will fill up your memory quickly.

Also, the code is currently only supports 64bit architectures, and this is hard-coded in many places.

There is no support for concurrency.

Why it might be interesting to you nevertheless

So if it is not really usable to run programs with, should you care about it? Probably not, but maybe you do for one of these reasons:

  • You always wondered how a compiler for Haskell actually works, and reading through a little over a thousands lines of code is less daunting than reading through the 34k lines of code that is GHC’s backend.
  • You have wacky ideas about Code generation for Haskell that you want to experiment with.
  • You have wacky ideas about Haskell that require special support in the backend, and want to prototype that.
  • You want to see how I use the GHC API to provide a ghc-like experience. (I copied GHC’s Main.hs and inserted a few hooks, an approach I copied from GHCJS).
  • You want to learn about running Haskell programs efficiently, and starting from veggies, you can implement all the trick of the trade yourself and enjoy observing the speed-ups you get.
  • You want to compile Haskell code to some weird platform that is supported by LLVM, but where you for some reason cannot run GHC’s runtime. (Because there are no threads and no garbage collection, the code generated by veggies does not require a runtime system.)
  • You want to formally verify Haskell code generation. Note that the code generator targets the same AST for LLVM IR that the vellvm2 project uses, so eventually, veggies can become a verified arrow in the top right corner map of the DeepSpec project.

So feel free to play around with veggies, and report any issues you have on the GitHub repository.

Birthday greetings communication behaviour

Published 2017-03-28 in sections English.

Randall Munroe recently mapped how he communicated with his social circle. As I got older recently, I had an opportunity to create a similar statistics that shows how people close to me chose to fulfil their social obligations (given the current geographic circumstances):

Communication variants

Communication variants

(Diagram created with the xkcd-font and using these two stackoverflow answers.)

In related news: Heating 3½ US cups of water to a boil takes 7 minutes and 40 seconds on one particular gas stove, but only 3 minutes and 50 seconds with an electric kettle, despite the 110V-induced limitation to 1.5kW.

(Diagram updated on March 30, as the actual mail is slower than the other channels.)

Why prove programs equivalent when your compiler can do that for you?

Published 2017-02-06 in sections English, Haskell.

Last week, while working on CodeWorld, via a sequence of yak shavings, I ended up creating a nicely small library that provides Control.Applicative.Succs, a new applicative functor. And because I am trying to keep my Haskell karma good1, I wanted to actually prove that my code fulfills the Applicative and Monad laws.

This led me to inserted writing long comments into my code, filled with lines like this:

The second Applicative law:

  pure (.) <*> Succs u us <*> Succs v vs <*> Succs w ws
= Succs (.) [] <*> Succs u us <*> Succs v vs <*> Succs w ws
= Succs (u .) (map (.) us) <*> Succs v vs <*> Succs w ws
= Succs (u . v) (map ($v) (map (.) us) ++ map (u .) vs) <*> Succs w ws
= Succs (u . v) (map (($v).(.)) us ++ map (u .) vs) <*> Succs w ws
= Succs ((u . v) w) (map ($w) (map (($v).(.)) us ++ map (u .) vs) ++ map (u.v) ws)
= Succs ((u . v) w) (map (($w).($v).(.)) us ++ map (($w).(u.)) vs ++ map (u.v) ws)
= Succs (u (v w)) (map (\u -> u (v w)) us ++ map (\v -> u (v w)) vs ++ map (\w -> u (v w)) ws)
= Succs (u (v w)) (map ($(v w)) us ++ map u (map ($w) vs ++ map v ws))
= Succs u us <*> Succs (v w) (map ($w) vs ++ map v ws)
= Succs u us <*> (Succs v vs <*> Succs w ws)

Honk if you have done something like this before!

I proved all the laws, but I was very unhappy. I have a PhD on something about Haskell and theorem proving. I have worked with Isabelle, Agda and Coq. Both Haskell and theorem proving is decades old. And yet, I sit here, and tediously write manual proofs by hand. Is this really the best we can do?

Of course I could have taken my code, rewritten it in, say, Agda, and proved it correct there. But (right now) I don’t care about Agda code. I care about my Haskell code! I don’t want to write it twice, worry about copying mistakes and mismatchs in semantics, and have external proofs to maintain. Instead, I want to prove where I code, and have the proofs checked together with my code!

Then it dawned to me that this is, to some extent, possible. The Haskell compiler comes with a sophisticated program transformation machinery, which is meant to simplify and optimize code. But it can also be used to prove Haskell expressions to be equivalent! The idea is simple: Take two expressions, run both through the compiler’s simplifier, and check if the results are the same. If they are, then the expressions are, as far as the compiler is concerned, equivalent.

A handful of hours later, I was able to write proof tasks like

app_law_2 = (\ a b (c::Succs a) -> pure (.) <*> a <*> b <*> c)
        === (\ a b c -> a <*> (b <*> c))

and others into my source file, and the compiler would tell me happily:

[1 of 1] Compiling Successors       ( Successors.hs, Successors.o )
GHC.Proof: Proving getCurrent_proof1 …
GHC.Proof: Proving getCurrent_proof2 …
GHC.Proof: Proving getCurrent_proof3 …
GHC.Proof: Proving ap_star …
GHC.Proof: Proving getSuccs_proof1 …
GHC.Proof: Proving getSuccs_proof2 …
GHC.Proof: Proving getSuccs_proof3 …
GHC.Proof: Proving app_law_1 …
GHC.Proof: Proving app_law_2 …
GHC.Proof: Proving app_law_3 …
GHC.Proof: Proving app_law_4 …
GHC.Proof: Proving monad_law_1 …
GHC.Proof: Proving monad_law_2 …
GHC.Proof: Proving monad_law_3 …
GHC.Proof: Proving return_pure …
GHC.Proof proved 15 equalities

This is how I want to prove stuff about my code!

Do you also want to prove stuff about your code? I packaged this up as a GHC plugin in the Haskell library ghc-proofs (not yet on Hackage). The README of the repository has a bit more detail on how to use this plugin, how it works, what its limitations are and where this is heading.

This is still only a small step, but finally there is a step towards low threshold program equivalence proofs in Haskell.


  1. Or rather recover my karma after such abominations such as ghc-dup, seal-module or ghc-heap-view.

Trump is so mean

Published 2017-01-29 in sections Philadelphia, Deutsch.

Vor zweieinhalb Monaten berichtete ich an dieser Stelle von meinen Eindrücken nach der Präsidentschaftswahl (Danke für die motivierenden Rückmeldungen!). Inzwischen ist Donald Trump Präsident, und nun geht es so richtig los.

Am Tag der Amtseinführung habe ich nicht viel mitbekommen. In Philadelphia gab wohl es Proteste, insbesondere am Tag drauf, als hier wie in vielen anderen Städten in und außerhalb der USA der „Women’s March“ statt fand. Über Facebook konnte ich mitverfolgen, welche meiner Bekannten teilnahmen, das war es aber auch erst mal.

Zumindest in Philadelphia halten viele wenig von Trumps Verordnungen

Zumindest in Philadelphia halten viele wenig von Trumps Verordnungen

Interessant wurden die nächsten Tage, als sich zeigte, dass Trump es ernst meint und mit einer Verfügung nach der anderen seine Vorstellungen in die Tag umsetzen wollte. Ich will hier nicht alles wiederholen, was schon ausführlichst in den Nachrichten, auch in Deutschland, behandelt wurde (die BBC hat eine gute Zusammenfassung der ersten Woche).

Für mich und mein akademisches Umfeld am relevantesten waren zwei Entwicklungen: Zum einen verfügte Trump einen Maulkorberlass für viele Behörden, und für das Umweltamt sogar einen kompletten Einstellungs- und Auftragstop, und von der Seite des Weißen Hauses verschwanden Abschnitte zum Klimawandel. Auch wenn sich ein paar Nationalparkranger dem Anfangs widersetzten – das ist nicht mehr ein Umfeld von freier Wissenschaft und Ratio-geleiteter Politik.

Noch heftiger war die Reaktion dann als Trump plötzlich und ohne Vorwarnung die Einreise von Bürgern sieben vorwiegend muslimischer Staaten, darunter dem Iran, stark einschränkte. Einige Reisende oder Wiederkehrende aus diesen Staaten wurden nun am Flughafen länger befragt, abgewiesen oder direkt zurückgeschickt. In meinem Freundeskreis hier sind auch Wissenschaftler aus dem Iran, deren Vertrauen in eine verlässliche Zukunft in den USA nun schwer beschädigt ist. Denn betroffen sind nicht etwa nur Bewerber um neue Visas, die sich nun auf längere Wartezeiten einstellen müssten, sondern auch solche, die schon längst ein Visum – oder gar eine permanente Aufenthaltsgenehmigung (green card)1 – haben und sich in den Staaten eine Existenz aufgebaut haben.

Eine Anspielung auf das bekannte Niemöller-Zitat

Eine Anspielung auf das bekannte Niemöller-Zitat

Über Facebook erfuhr ich dass einige meiner Freunde, insbesondere eben jene Iranerin, an einer spontanen Demonstration heute Nachmittag am Flughafen von Philadelphia teilnehmen wollten, und dem schloss ich mich an. Allerings nicht nur ich, so dass schon die Autobahn zum Flughafen von den Autos empörter Bürger verstopft war und zeiweise die Autobahnausfahrten gesperrt waren.

Einige parkten weiter weg und liefen zum Flughafen (und waren schneller)

Einige parkten weiter weg und liefen zum Flughafen (und waren schneller)

Die Empfangshalle des Flughafens, dem angedachten Ort für den Protest, war angesichts von über 5000 Teilnehmern schon längst voll. Die in großer Zahl (und mit Pferden) aufmaschierte Polizei sperrte den Zugang und verlegte den Protest vor das Gebäude.

Eines von vielen Kindern auf der Demo

Eines von vielen Kindern auf der Demo

Ich mischte mich also eine Weile unter das dort protestierende Volk, lauschte den Sprechchören („No hate, no fear – refugees are welcome here“, „Let them in“, „This is what democracy looks like“) und bewunderte die unzähligen Pappschilder. Die Bilder hier sind eine Auswahl der besten (und weitere gibt es auf meiner Bilderseite).

So etwas wie Beamtenbeleidigung kennt man im Land der free speech nicht

So etwas wie Beamtenbeleidigung kennt man im Land der free speech nicht

Global almost-constants for Haskell

Published 2017-01-20 in sections English, Haskell.

More than five years ago I blogged about the “configuration problem” and a proposed solution for Haskell, which turned into some Template Haskell hacks in the seal-module package.

With the new GHC proposal process in plase, I am suddenly much more inclined to write up my weird wishes for the Haskell language in proposal form, to make them more coherent, get feedback, and maybe (maybe) actually get them implemented. But even if the proposal is rejected it is still a nice forum to discuss these ideas.

So I turned my Template Haskell hack into a proposed new syntactic feature. The idea is shamelessly stolen from Isabelle, including some of the keywords, and would allow you to write

context fixes progName in
  foo :: Maybe Int -> Either String Int
  foo Nothing  = Left $ progName ++ ": no number given"
  foo (Just i) = bar i

  bar :: Int -> Either String Int
  bar 0 = Left $ progName ++ ": zero no good"
  bar n = Right $ n + 1

instead of

foo :: String -> Maybe Int -> Either String Int
foo progName Nothing  = Left $ progName ++ ": no number given"
foo progName (Just i) = bar progName  i

bar :: String -> Int -> Either String Int
bar progName 0 = Left $ progName ++ ": zero no good"
bar progName n = Right $ n + 1

when you want to have an “almost constant” parameter.

I am happy to get feedback at the GitHub pull request.

TikZ aesthetics

Published 2017-01-06 in sections English, Digital World.

Every year since 2012, I typeset the problems and solutions for the German math event Tag der Mathematik, which is organized by the Zentrum für Mathematik and reaches 1600 students from various parts of Germany. For that, I often reach to the LaTeX drawing package TikZ, and I really like the sober aesthetics of a nicely done TikZ drawing. So mostly for my own enjoyment, I collect the prettiest here.

On a global scale they are still rather mundane, and for really impressive and educating examples, I recommend the TikZ Gallery.

microG on Jolla

Published 2016-11-23 in sections English, Digital World.

I am a incorrigibly in picking non-mainstream, open smartphones, and then struggling hard. Back then in 2008, I tried to use the OpenMoko FreeRunner, but eventually gave up because of hardware glitches and reverted to my good old Siemens S35. It was not that I would not be willing to put up with inconveniences, but as soon as it makes live more difficult for the people I communicate with, it becomes hard to sustain.

Two years ago I tried again, and got myself a Jolla phone, running Sailfish OS. Things are much nicer now: The hardware is mature, battery live is good, and the Android compatibility layer enables me to run many important apps that are hard to replace, especially the Deutsche Bahn Navigator and various messengers, namely Telegram, Facebook Messenger, Threema and GroupMe.

Some apps that require Google Play Services, which provides a bunch of common tasks and usually comes with the Google Play store would not run on my phone, as Google Play is not supported on Sailfish OS. So far, the most annoying ones of that sort were Uber and Lyft, making me pay for expensive taxis when others would ride cheaper, but I can live with that. I tried to install Google Play Services from shady sources, but it would regularly crash.

Signal on Jolla

Now in Philadelphia, people urged me to use the Signal messenger, and I was convinced by its support for good end-to-end crypto, while still supporting offline messages and allowing me to switch from my phone to my desktop and back during a conversation. The official Signal app uses Google Cloud Messaging (GCM, part of Google Play Services) to get push updates about new posts, and while I do not oppose this use of Google services (it really is just a ping without any metadata), this is a problem on Sailfish OS.

Luckily, the Signal client is open source, and someone created a “LibreSignal” edition that replaced the use of GCM with websockets, and indeed, this worked on my phone, and I could communicate.

Things were not ideal, though: I would often have to restart the app to get newly received messages; messages that I send via Signal Desktop would often not show up on the phone and, most severe, basically after every three messages, sending more messages from Desktop would stop working for my correspondents, which freaked them out. (Strangely it continued working from their phone app, so we coped for a while.)

So again, my choice of non-standard devices causes inconveniences to others. This, and the fact that the original authors of Signal and the maintainers of LibreSignal got into a fight that ended LibreSignal discontinued, meant that I have to change something about this situation. I was almost ready to give in and get myself a Samsung S7 or something boring of the sort, but then I decided to tackle this issue once more, following some of the more obscure instructions out there, trying to get vanilla Signal working on my phone. About a day later, I got it, and this is how I did it.

microG

So I need Google Play Services somehow, but installing the “real thing” did not seem to be very promising (I tried, and regularly got pop-ups telling me that Play Services has crashed.) But I found some references to a project called “microG”, which is an independent re-implementation of (some of) of the play services, in particular including GCM.

Installing microG itself was easy, as you can add their repository to F-Droid. I installed the core services, the services framework and the fake store apps. If this had been all that was to do, things would be easy!

Play Store detection work arounds

But Signal would still complain about the lack of Google Play Services. It asks Android if an app with a certain name is installed, and would refuse to work if this app does not exist. For some reason, the microG apps cannot just have the names of the “real” Google apps.

There seem to be two ways of working around this: Patching Signal, or enabling Signature Spoofing.

The initially most promising instructions (which are in a README in a tarball on a fishy file hoster linked from an answer on the Jolla support forum…) suggested patching Signal, and actually came both with a version of an app called “Lucky Patcher” as well as a patched Android package, but both about two years old. I tried a recent version of the Lucky Patcher, but it failed to patch the current version of Signal.

Signature Spoofing

So on to Signature Spoofing. This is a feature of some non-standard Android builds that allow apps (such as microG) to fake the existence of other apps (the Play Store), and is recommended by the microG project. Sailfish OS’s Android compatibility layer “Alien Dalvik” does not support it out of the box, but there is a tool “tingle” that adds this feature to existing Android systems. One just has to get the /system/framework/framework.jar file, put it into the input folder of this project, run python main.py, select 2, and copy the framework.jar from output/ back. Great.

Deodexing Alien Dalvik

Only that it only works on “deodexed” files. I did not know anything about odexed Android Java classes (and did not really want to know), but there was not way around. Following this explanation I gathered that one finds files foo.odex in the Android system folder, runs some tool on them to create a classes.dex file, and adds that to the corresponding foo.jar or foo.apk file, copies this back to the phone and deletes the foo.odex file.

The annoying this is that one does not only have to do it for framework.jar in order to please tingle, because if one does it to one odex file, one has to do to all! It seems that for people using Windows, the Universal Deodexer V5 seems to be a convenient tool, but I had to go more manually.

So I first fetched “smali”, compiled it using ./gradlew build. Then I fetched the folders /opt/alien/system/framework and /opt/alien/system/app from the phone (e.g. using scp). Keep a backup of these in case something breaks. Then I ran these commands (disclaimer: I fetched these from my bash history and slightly cleaned them up. This is not a fire-and-forget script! Use it when you know what it and you are doing):

cd framework
for file in *.odex
do
  java -jar ~/build/smali/baksmali/build/libs/baksmali.jar deodex $file -o out
  java -jar ~/build/smali/smali/build/libs/smali.jar a out -o classes.dex
  zip -u $(basename $file .odex).jar classes.dex
  rm -rf out classes.dex $file
done
cd ..

cd app
for file in *.odex
do
  java -jar ~/build/smali/baksmali/build/libs/baksmali.jar deodex -d ../framework $file -o out
  java -jar ~/build/smali/smali/build/libs/smali.jar a out -o classes.dex
  zip -u $(basename $file .odex).apk classes.dex
  rm -rf out classes.dex $file
done
cd ..

The resulting framework.jar can now be patched with tingle:

mv framework/framework.jar ~/build/tingle/input
cd ~/build/tingle
./main.py
# select 2
cd -
mv ~/build/tingle/output/framework.jar framework/framework.jar

Now I copy these framework and app folders back on my phone, and restart Dalvik:

devel-su systemctl restart aliendalvik.service

It might start a bit slower than usually, but eventually, all the Android apps should work as before.

The final bit that was missing in my case was that I had to reinstall Signal: If it is installed before microG is installed, it does not get permission to use GCM, and when it tries (while registering: After generating the keys) it just crashes. I copied /data/data/org.thoughtcrime.secretsms/ before removing Signal and moved it back after (with cp -a to preserve permissions) so that I could keep my history.

And now, it seems, vanilla Signal is working just fine on my Jolla phone!

What’s missing

Am I completely happy with Signal? No! An important feature that it is lacking is a way to get out all data (message history including media files) in a file format that can be read without Signal; e.g. YAML files or clean HTML code. I do want to be able to re-read some of the more interesting conversations when I am 74 or 75, and I doubt that there will be a Signal App, or even Android, then. I hope that this becomes available in time, maybe in the Desktop version.

I would also hope that pidgin gets support to the Signal protocol, so that I conveniently use one program for all my messaging needs on the desktop.

Finally it would be nice if my Signal identity was less tied to one phone number. I have a German and a US phone number, and would want to be reachable under both on all my clients. (If you want to contact me on Signal, use my US phone number.)

Alternatives

Could I have avoided this hassle by simply convincing people to use something other than Signal? Tricky, at the moment. Telegram (which works super reliable for me, and has a pidgin plugin) has dubious crypto and does not support crypto while using multiple clients. Threema has no desktop client that I know of. OTR on top of Jabber does not support offline messages. So nothing great seems to exist right now.

In the long run, the best bet seems to be OMEMO (which is, in essence, the Signal protocol) on top of Jabber. It is currently supported by one Android Jabber client (Conversations) and one Desktop application (gajim, via a plugin). I should keep an eye on pidgin support for OMEMO and other development around this.