External Content not shown. Further Information.

Popular Culture:

• Eine Tonne Schokolade Ausgelaufen

Nerd Culture:

• INPUT 64 ist ein von 1985 bis 1988 im Heise-Verlag erschienenes Computermagazin für den Commodore 64, das aus einer Kassette oder Diskette, sowie einem Begleitheft bestand. (via)

STEM/MINT:

• Bluetooth-equipped capsule communicates from the gut – bald gibt es Cloud-Retardierung.
• 300 years of element discovery
• 34 erstaunliche Zecken-Fakten!
• Siberian Worms Buried in Arctic Permafrost for 42,000 Years Come Back to Life
• vdash: a formal math wiki

Software/Programming:

• A cross-platform, GPU-accelerated terminal emulator – for your high-end-TUI.
• Library for using generic and type safe container in pure C99 language for a wide collection of container
• awesome awesomeness
• Parse command line argument by defining a struct in Rust
• Rust Emacs
• Convert your ascii diagram scribbles into happy little SVG
• LaTTe : a Laboratory for Type Theory experiments (in clojure) (via)
• Why I'm usually unnerved when modern SSDs die on us
• Silbentrennung per CSS3
• Ein Twitch-Streamer ist der größte Albtraum aller Telefonbetrüger – I like the videos :3

WTF:

• NSFW: Glass Vibrator Urn
• High School Student Injects The Book Of Genesis Into His Body (via) – but why?
• Russian Bears Are Hooked on Huffing Jet Fuel Until They Pass Out

Zeroth World/SciFi becoming Reality:

• Hartnäckige Bakterien auf der ISS

Art (Comics etc.):

• Monkey
• Snowflake
• Pills
• Okay
• Don't smoke marijuana!
• Gift Bearer

Quotes:

• If you try to design something idiot proof the universe will just design a better idiot.
• Datenbanken sind doch auch nur Multiplayerexcel.
• Neil Armstrong was the first man to land on the moon. "Neil A." backwards is "Alien"

And again, I gave a talk for the best mathematics club of the multiverse, for "younger" students, meaning that this text is not scientific. This is the script for the talk.

We want to prove the following theorem:

Theorem: There is an algorithm of which, with standard set theory, we cannot decide whether it terminates.

Firstly, we need to look at what an algorithm is. Usually, people introduce this with Turing machines. However, we will use a model which is closer to modern computers, so-called register machines. These are provably equivalent to Turing machines, except that some algorithms might take a bit longer on Turing machines – but at this point, we do not care about efficiency, we just care about whether things can be calculated at all, given enough time and space. If you care about efficiency, that would be in the realm of complexity theory, while we will work in the realm of recursion theory.

A register machine has a finite set of registers R[0], R[1], …, which can contain arbitrarily large natural numbers. A program consists of a sequence of instructions:

• For every i, there is the instruction R[i]++, which increases the number that is contained in R[i].
• For every i, there is the instruction R[i]--, which decreases the number contained in R[i] if it is larger than 0, and does nothing otherwise.
• There is the instruction End, which ends the program.
• For every i and n, there is the instruction if R[i]==0 then goto n. The instructions are numbered, and this instruction jumps to the instruction with number n, if R[i] contains 0, otherwise it does nothing.

The following program checks whether R[0] >= R[1], and if so, it sets R[2] to 1:

0 if R[1]==0 then goto 6
1 if R[0]==0 then goto 5
2 R[1]--
3 R[0]--
4 if R[2]==0 then goto 0
5 End
6 R[2]++
7 End

Line 4 is only here to do an unconditional jump, therefore, we can introduce a shorthand that just does an unconditional jump:

0 if R[1]==0 then goto 6
1 if R[0]==0 then goto 5
2 R[1]--
3 R[0]--
4 goto 0
5 End
6 R[2]++
7 End

To make it a bit more readable, we can omit the line numbers, which we usually do not need, and just set labels to the lines we want to jump to:

Start: if R[1]==0 then goto Yes
if R[0]==0 then goto No
R[1]--
R[0]--
goto Start

No: End

Yes: R[2]++
End

This just increases readability, it doesn't make anything possible that wasn't possible before. By using this algorithm, we can generally check whether R[i] > R[j], and therefore, we can introduce a shorthand notation if R[i] > R[j] then goto A without being able to do anything we couldn't do before.

We can do addition by

Start: if R[1]==0 then goto Done
R[0]++
R[1]--
goto Start
Done: End

and truncated subtraction () by

Start: if R[1]==0 then goto Done
R[0]--
R[1]--
goto Start
Done: End

Therefore, we can add the instructions R[i]+=R[j] which adds R[j] to R[i], and R[i]-=R[j], without being able to do anything more than before. Having these instructions, we can define multiplication by repeated addition, and division and modulo by repeated subtraction. This is left to the reader.

Now, we cannot know for sure whether everything that is computable at all is computable by register machines. However, we do not know any computable function that cannot be computed by a register machine. Hence, it is generally believed that there is none. This is called the Church-Turing thesis.

These programs operate on numbers only. Real computers work with images and text. However, this is, computationally, no difference, and there are several injections between these kinds of data. Especially, programs themselves can be represented as numbers, which is called Gödelization. For this, we use the Cantor Pairing, which gives a bijective function by . This function enumerates the backward diagonals on the grid of natural numbers, as this graphic shows. The pairing itself can obviously be calculated with the above functions by a register machine. Inverting the function is also easy, and left to the reader.

Now we can represent every program we have in the following way: We first map numbers to the single instructions:

• R[i]++ is mapped to
• R[i]-- is mapped to
• if R[i]==0 then goto j is mapped to
• End is mapped to

Therefore, every instruction has its own code. A program can be encoded as a sequence of these codes; the program with the instructions can be encoded by .

Therefore, it is well-defined to talk about "programs getting other programs as parameters". And having seen this, it is easy to write an universal register machine, which evaluates such a program, given a sequence of register values:

The state of a program is entirely determined by its registers and the number of the current instruction. It has a finite sequence of registers , and an instruction line , and therefore, we can encode the state by .

Now, let contain the program code, and contain the current state. Let be the first element of the program state, which tells us, at which position of we are. Let be the current instruction given by .

• If , let and . is the value of the -st register in the simulated program. We replace it inside by and replace by . We simulated R[k-1]++.
• Similarily, we can simulate R[k-1]--.
• For , we have to check the register value, and set the instruction number to the apropriate value.
• For , we end, and have the final state of the program.

While it is really intricate, we can see that it is possible to "simulate" a register program inside a register program. A natural question which arises is: Is there an algorithm such that, given a program (or its Gödelization), and an input state , the algorithm determines whether terminates. This problem is called the Halting problem. We now show that it cannot be solved. Formally, we show that there is no program that, given the Gödelization of a program in and an input state in , leaves being 0 if and only if with the given input state terminates. We do this by contradiction: Assume such an M exists. Then we could, from this M, generate the following program:

"execute M"
if R[2]==0 then goto Loop
End
Loop: goto Loop

This program terminates if and only if the given program with the given state does not terminate. We modify this program once again by one line:

"set R[1] to <R[0]>"
"execute M"
if R[3]==0 then goto Loop
End
Loop: goto Loop

We call this program . only takes one argument. It terminates if and only if the given program, given its own Gödelization, does not terminate. Such programs are called self-accepting.

Now, as is itself a program, we can Gödelize it, so let be the Gödelization. By setting , we can calculate .

Now assume terminates. This means that in after executing M there will be R[2]==0. Therefore would not terminate. Contradiction.

But assuming would not terminate would mean, by the same argument, that R[2] is not 0 after M. Therefore, would terminate. Also a contradiction.

Such a program cannot exist. Therefore, cannot exist.

This proves that we cannot generally decide whether an algorithm terminates. However, it is not yet what we want: We want an algorithm, of which we cannot decide whether it terminates, at all. To get it, we need to do a bit of logic. We will mainly focus on Zermelo-Fraenkel set theory here, as it is the foundation of mathematics.

We first define what a mathematical formula is, which is essentially a string that encodes a mathematical proposition.

• We have an infinite set of variable symbols .
• The set of strings is the set of atomic formulae: Formulae which just give them -relation between two free variables.

Now, the set of formulae is the smallest set, such that

• Every atomic formula is a formula: .
• If and , then ("for all a X holds") and ("there exists an a such that X holds") and ("not X") are in .
• If , then ("X and Y"), ("X or Y") and ("X implies Y") are in .

We now give the axioms of set theory:

NUL: There is an empty set:

We can introduce a common shorthand notation for by , and rewrite this axiom as

If we want to talk about the empty set now, we need to introduce some variable , and add to the formula. Therefore, our system doesn't get stronger if we introduce a symbol for the empty set, instead of always adding this formula, and it increases readability, which is why we do that.

We furthermore define the shorthand notation by , and by .

EXT: The axiom of extensionality says that sets that contain the same elements are also contained in the same sets:

FUN: The axiom of foundation says that every set contains a set that is disjoint to it. From this axiom follows that there are no infinite -chains.

or, with additional obvious shorthand notation

PAR: The axiom of pairing says that there is a set that contains at least two given elements, meaning, for all , there exists a superset of :

UN: The axiom of union says that the superset of the union of all sets in a set exists:

POW: The axiom of the powerset: A superset of the powerset of every set exists:

.

INF: The axiom of infinity says that a superset of the set of natural numbers exists. Natural numbers are encoded as ordinals: , and . Writing it out as formula is left as an exercise.

The other two sets of formulae we need are given by axiom schemes: They are infinitely many axioms, but they can be expressed by a simple, finite rule:

SEP: The axiom scheme of separation says that, for every formula and every set , the set exists:

Let a formula be given with free variables among , and not occur freely. Then the formula

.

is an axiom of set theory.

RPL: The axiom scheme of replacement is a bit more complicated.

A formula is called a functor on a set (which is not the same as a functor in category theory), if for all there is a unique such that holds. Therefore, in some sense, defines something similar to a function on , and we write for this unique . Then the set , the "image" of , exists. Formalizing this scheme is left as an exercise.

AC: It should be noted that usually the axiom of choice is added. However, we do not need to care whether it is added or not, so we omit it here.

We already talked about embedding natural numbers into this set theory. We can also define general arithmetic inside this set theory. Most of mathematics can be formalized inside Zermelo-Fraenkel set theory.

Now, we can formalize propositions. Now we want to formalize proofs. Normally, I would introduce the calculus of natural deduction here, because it corresponds to the dependently typed lambda calculus, so every proof is a term. However, for the specific purpose we need, namely, formalizing proof theory in arithmetic, the equivalent Hilbert calculus is the better choice. It corresponds to the SKI calculus for proof terms.

Firstly, we further reduce our formulae: We can express as , and as . Furthermore, can be expressed by . Hence, we only need , and to express all formulae. We now define additional logical axiom schemes, where range over all formulae. (Notice: is right-associative.)

• P1.
• P2.
• P3.
• Q5. for all variables
• Q6.
• Q7. if is not free in

A proof of a formula is a finite sequence of formulae , such that and for all , either is an axiom of set theory, or a logical axiom, or there exist such that . Essentially this means that everything in the formula is either an axiom or follows from former formulae applying modus ponens.

Completeness Theorem: If a formula is true in set theory, then there exists a proof of it.

To prove this, we would need model theory, which would lead too far, so we leave out the proof.

Now, as we did for programs before, we can gödelize formulae and proofs. Let us denote by the gödelization of .

Diagonalization Lemma: For every formula with one free variable , there exists a formula , such that holds.

Proof: First, we notice that, given the formula , we can express the substitution of another variable for , therefore, we can give a function that satisfies . Now we can define . Now, define . Then we have . This concludes the proof.

Notice that the definition of is computational: It can be done effectively by a computer. As we can find such a formula for every , we denote it by .

Now, we can also gödelize proofs and their correctness criterion. Therefore, we can give a formula meaning " is the gödelization of a correct proof of the gödelized formula ". Therefore, says that the gödelized formula is provable.

By the diagonalization lemma, there is a formula such that . Now, assume that does not hold. Then also cannot hold, therefore, it would be provable, which is a contradiction. Hence, must hold. But then, it cannot be provable. This is a (sketch of a) proof of

Gödel's first incompleteness theorem: In Zermelo-Fraenkel set theory, there are propositions that can neither be proved nor disproved.

More generally, this theorem holds for all axiom systems that are capable of basic arithmetic, because this is all we used. Specifically for Zermelo-Fraenkel set theory, there are other examples of such propositions, namely the continuum hypothesis, and the existence of large cardinals.

Now, something we always implicitly assumed is that set theory is consistent: If is provable, then cannot be provable. This is, however, unknown, which follows from:

Gödel's second incompleteness theorem: Set theory cannot prove its own consistency.

Proof: We use our from the proof of the first incompleteness theorem. Furthermore, we can define such that . Now, we can define what it means to be consistent, namely: . Now, we know that , and therefore, since false propositions imply anything, for all formulae , and obviously this implies . Therefore, . But this contradicts what we proved in the first completeness theorem. Hence, cannot be provable.

Let . Obviously, if and only if set theory is inconsistent (since it is wrong). Now consider the following algorithm:

Retry: if ν(R[0], a) then goto Found
R[0]++
goto Retry
Found: end

Does this algorithm terminate?

If it terminates, it has found an inconsistency in set theory. Assuming that set theory is consistent, it would not terminate. But if we could prove that it does not terminate, we would be able to prove that set theory is consistent, and this contradicts the second incompleteness theorem.

Hence, we have an algorithm of which we cannot decide whether it terminates.

External Content not shown. Further Information.

Nerd Culture:

• MIT researchers create a robot houseplant that moves on its own (via) – has science gone too far?
• A Portal Port Programmed For Platforms Of The Past
• Six Degrees of Wikipedia (via)
• The blue eyed islanders puzzle
• Mensa Online-Test

STEM/MINT:

• Mitochondrial DNA Can Be Inherited From Fathers (via)
• Record-breaking atomic clocks precise enough to measure spacetime distortions

Software/Programming:

• Google, Mozilla working on letting web apps edit files despite warning it could be 'abused in terrible ways' (via)
• The Kernel Underground
• Microsoft to Silently Remove the CONCATENATE Function from Excel, Offers Paid Alternative: CONCAT
• Quiz zum Tag der Computersicherheit
• Compiler basics: lisp to assembly (via)

WTF:

• L’Oréal’s Smart Hairbrush (via)

Art (Comics etc.):

• Nudist Colony

External Content not shown. Further Information.

Politics/Law:

• Die Frage nach dem Sinn des Mathematikunterrichts
• Unterweisung der Jugend

Popular Culture:

• UN report reveals ozone layer on track for full recovery by 2060
• Das Leid der Turbo-Kühe

Nerd Culture:

• C Portability Lessons from Weird Machines (via)

STEM/MINT:

• Rowhammer on ECC Memory
• NSFW: Molecules with Silly or Unusual Names

Software/Programming:

• When does white space matter in HTML?
• C++20 wird fast eine richtige Programmiersprache

WTF:

• „Cyber Kitchen“: Deutsche Telekom bringt Kochbuch raus
• Katholische Kirche bringt Pokémon-Klon
• A bra that falls off when you clap your hands (new patent)

Art (Comics etc.):

• NSFW Face Recognition
• carchaeology
• What coders really want

External Content not shown. Further Information.

Politics/Law:

• Straftäter dürfen Bitcoins nicht behalten – "Auch der Einwand, dass die Behörden ohne Kenntnis des privaten Schlüssels nicht auf die Wallets der Angeklagten zugreifen könnten, ändert hieran nichts. Das sei eine reine Vollstreckungsfrage, so das Gericht."
• Kommentar zur IoT-Sicherheit: Europas Verordnung ist zahnlos – was ich ja immer nicht verstehe ist, wieso es nicht einfach standardmäßig so ist, dass die Hersteller in vollem Umfang haftbar gemacht werden können?

STEM/MINT:

• Lumen in Watt richtig umrechnen
• BIGNUM BAKEOFF contest recap "The aim of this contest was to write a C program of 512 characters or less (excluding whitespace) that returned as large a number as possible from main(), assuming C to have integral types that can hold arbitrarily large integers. [...] The final and winning entry, {loader.c}, diagonalizes over the Huet-Coquand `calculus of constructions'."
• Ein BIOS-Update von Lenovo Ziegelsteint die Rechner – es geht um irgendwas mit Thunderbolt. Man sollte halt das BIOS vielleicht nicht zu oft verändern, und vielleicht auch nicht zu komplex gestalten.
• Typesetting modal logic
• iPhones are Allergic to Helium
• Psychedelic psilocybin therapy for depression granted Breakthrough Therapy status by FDA
• World-first aerogel is made from plastic bottles
• How to implement strings – maybe interesting for beginners (or people who never used any low-level programming language).
• Cookie Editor for Chrome-Bases Browsers
• GSM-Codes: Befehle für das Mobilfunknetz
• C-QUIZ
• pointers are more abstract than you might expect in C
• Orgmode for GTD

WTF:

• Der Generalinspekteur der Panzertruppen - Die Tiger-Fibel
• Es gibt jetzt Segensroboter (via)

Art (Comics etc.):

• Good Times
• Problem
• Moon
• Regenbogenflagge
• Meinungsfreiheit

Quotes:

• It's terrifying that both of these things are true at the same time in this world: 1. Computers drive cars around. 2. the state of the art test to check that you are not a computer is whether you can successfully identify stop signs in pictures.

Nie dürft ihr so tief sinken, von dem Kakao, durch den man euch zieht, auch noch zu trinken.

- Erich Kästner

So I bought a new smear^H^H^H^H^Hsmartphone. My old phone was fine, it was a Moto G5, but somehow the developers thought that an exchangable battery is an excuse for not including a compass – but I often use it to navigate, and that sucks without a compass. Now I bought a Moto G6, which has a compass, but no easily exchangable battery, and a fingerprint sensor that is even worse than the one from the Moto G5.

Not being able to easily exchange the battery is the current trend. I chose the Moto G6 because at least it seems to be doable to exchange the battery at some point. I want a phone which I can have for longer than two years. And I think one reason for not having an exchangable battery is to make people buy new phones after about two years, because that is usually the time, in my experience, when batteries lost a relevant amount of duration. It is an instance of Planned Obsolescence.

Which brings me right to the point: The whole ecosystem around Android is a big capitalist circlefuck. Android has created an immune system against software freedom and personal freedom.

So when starting my new phone, the shiny motorola start animations shalmed right back at me. Then I was asked to enter my SIM code and connect to Wifi. Then I was asked whether I wanted to import settings from another phone, which I wanted, so I started the procedure and hoped that my app settings would be synced.

After that, I was kindly asked to connect my Google account with Outlook, because reasons. I accidentally did that, now Microsoft can access my Mails from Google I guess(?). Well, why not. I mean, Outlook appears to be the default Mail application on this phone. I have no idea why anyone would want that instead of the original GMail app, but just as a wild guess, one could think of the possibility that Microsoft might have payed for that.

After that, there was a system upgrade, and lots of "system apps" were updated. "System apps" are apps you cannot uninstall. One would assume that these apps are essential for the system to work. But to be honest, I do not see why "LinkedIn" is an essential app. Again, one might think of the possibility that LinkedIn &c payed for that.

Then I was asked to configure the fingerprint reader, and got some messages from these "system apps" telling me that they are there and why I should use them or something … I just closed them. There were two reasons for choosing a Moto G6: The first reason was that I hoped it would be similar to the Moto G5. I don't see that. The UI is entirely different. The second reason is that the older Moto G phones are supported by Lineage OS, so I hope that in the future, it will also be supported. That is important, because the vendors stop supporting their phones at some point – which is also planned obsolescense, but also creates a huge security hazard. There should be laws against this practice – but that will probably not happen in Europe.

Update: I was told that Lineage OS still uses proprietary blobs as its drivers, which may contain security holes but can only be fixed by the companies that made them. Replicant doesn't do that, but won't run on as many devices, therefore.

Now even though I used the official sync functionality, most things just have not been synced. Like, everything useful was not synced. My app settings for Conversations and K9 Mail for example. Also my WhatsApp contacts and logs were not synced. I restored a backup, but only to learn that it lost messages. Because this is not how Android works. In theory, as it is a single-user system, there could be some central place where apps store their configuration. Think of the windows registry or dconf. Instead, apps get their directories in which they place SQLite3 databases.

Which brings me to the next point: The filesystem. Yes, Android has one, but tries to hide it. I do not understand why hiding the filesystem is so trendy right now. Hierarchical filesystems are good, clean, simple and easy to understand. They are a perfect example of an abstraction that is easily usable by humans, as well as efficiently implementable for computers. On Android, it can be hard to create a file with one app, and open it with another app, even though they are on the same computer. This got on my nerves several times. And people start to think it has to be this way. It hasn't. Having access to a cleanly structured filesystem is strictly better than whatever Android does.

And since sending a file to another app on your same phone is so hard, it can be almost impossible to get some file from your computer to your phone (let alone saving it in the right place and making the corresponding apps open it). I have seen people use DropBox for this several times, even though the two computers were in the same room. And for the providers, this makes sense: It makes you use more traffic, and it makes you upload more files, so they can be scanned into your ad profile.

This brings me to another point: The connectivity. It is assumed that you have a fast internet connection with no traffic limits. Many apps assume this. YouTube does not properly cache its videos, except when you explicitly download them. Chrome always reloads tabs when they went out of focus too long. There is no caching done. I have also seen some apps profiling your network connection to decide how much bloat to download. All of this assumes that you have an infinite amount of traffic. But of course, this is good for your internet providers: As there is still no affordable real flatrate for mobile internet in Europe, you will have to pay for additional traffic.

However, still, a smartphone is a highly portable computer, and as such, often changes places, and therefor often switches between networks. That is a problem for chat applications which need to manage their persistent connection. Also, sending keep-alive-packets will drain battery. In theory, TCP with the right parameters should be able to handle this. In practice, programmers do not know this. Hence, Google invented cloud messaging: Your app registers a server, which connects to Google servers, and sends messages. Google play services will itself keep an XMPP-connection to the Google servers, and forward those messages to the registered apps.

The problem is that your app needs to be from Google play. F-Droid apps cannot do this. Another problem is that the push server is hardcoded into the app. That is especially bad for free decentral services like XMPP: I am hosting an XMPP server, and Conversations is a very good client, but the version supporting cloud push costs a few euros, because they have to host an own cloud push server. To prevent this, I would also host an own cloud push server. But to do this, I would need to recompile the app and put it into the Google play store. Which is stupid, considering the fact that it would cost me money, and it would publish my Conversations fork for everyone, while I just want the people with an uxul.de-Account to use it. In the meantime, there might be an alternative, HTML5 Web Push. Maybe there will be support for this in some web client like converse.js in the future. At the moment, there isn't.

The App store is a problem of its own. In theory, having an app store is a good thing. It can improve security, because one can quickly react to security holes. It also can do dependency tracking. In theory, it is like a good old package repository, think of Debian/Ubuntu. In practice, there appears not to be any dependency management, and every app just bundles all of its dependencies, because a few hundred megabytes for a mail client is not a reason not to use it, aparently. Also, it costs money. Not much money, but it costs money. Commercial apps have no problem: Hosting a push server in AWS is cheap. And WhatsApp and Telegram are free as in free beer, and work out of the box.

Of course, they collect your data. Yes, they are encrypted, but at least they know your friends, and they know when you are awake. I would guess that automatically reading your address book entries should be illegal. The Facebook Messenger at least asks whether he may access the address book. They make you the criminal.

Android kills background applications, except when you explicitly allow them to run. This is one further reason for cloud push. And this really gets on my nerves sometimes. I often use Google Maps and the Deutsche-Bahn-Navigator. I want these to stay open, so I can look up things again afterwards. However, it seems that they are reaped from time to time. And they will not always go back to the state where I left them. This is annoying. Of course, you do not have to worry about closing programs anymore, as you would have on a normal computer. But I do not really see the great advantage in that. I also do not see why they do not support swapping.

People often argue that my opinions assume that smartphones are computers. They do. But I don't see why smartphones are not computers. They are small, highly portable computers, with lots of sensors and a touchscreen. The touchscreen is the main difference to laptops and notebooks. And for computers, there is a set of principles that work: The UNIX principles.