(Source: Gifbin)

As for most computer scientists, I always think about the features I would include into a programming language. Though I will probably never actually implement one (it is a lot of work, and there are plenty of languages already there), thinking about it can lead to interesting questions and insights. One such insight is that any practical language should have an exception system – which, however, should only be used in actually exceptional situations.

Why exceptions at all?

In theory, everything is embeddable in an Exception monad (or a sum type). But some exceptions can always happen, for example OOM. Or a system signal.

There are lots of algorithms that only work when everything goes right. A parser that returns a cototal AST, which is consumed lazily by an algorithm, for example. (Update: Seems like for such cases, Iteratees are better-suited.)

Verification of such algorithms can be tedious when one always has to cope with the possibility of failure. Abstracting very uncommon failures away into exceptions should be possible in a type-safe way. However, of course, they bloat the type system. Therefore, an Exception-system should mainly contain the possibility to safely unroll the call-stack and return the program into a safe and well-defined state.

For example, Lisp's way of communicating across the borders of stack frames and defining restarts is elegant and well-suited for rapid prototyping, but too general for formal verification. Such constructs should only be used with sophisticated monads, or given as parameters, but do not really fit into strictly typed languages, I think.

Criteria for exceptions

Exceptions should only be thrown in exceptional situations. I worked out the following three three criteria:

1. The problem must be something unlikely that usually does not happen.

2. Not unrolling and aborting would leave the program in an indefinite state.

3. The program cannot really do anything about it, or at least doing anything about it is not in the domain of the current subroutine.

Examples

These are not sharp criteria. There are many cases where it is debatable. In the end, they are more guidelines for API design. I came up with these when thinking about several examples:

• The filesystem gets out of memory: While writing a file, that is something unlikely. One should close and maybe delete the file afterwards. The program cannot do anything about it, since this is something the system has to cope with. However, when using fallocate(2), returning an error is a well-defined behavior, and should not result in an exception.

• The program runs out of memory: Also something unlikely with sophisticated memory management. However, this exception may be thrown by custom allocators, but not by explicit calls to malloc(3) and the like. Because malloc(3) returning NULL is well-defined behavior. If your custom allocator cannot allocate, then it may throw an exception. malloc(3) itself or similar raw abstractions over it should not.

• End-of-File while reading: Files are usually finite. This is nothing unexpected. It can, of course, be unexpected when parsing something. But then, this is a parser exception, not an exception about the EOF itself.

If you have any opinion about it, feel free to let me know.

External Content not shown. Further Information.

Liebe Anbieter des mobilen Zwischennetzes. Ihr habt das Netz wunderbar mit LTE ausgebaut. Wohl nicht unerheblich mit Steuergeldern, dennoch honoriere ich das sehr, denn das Internet ist ein wichtiger kultureller Faktor geworden, und jeder sollte Zugriff darauf haben.

Aber: Ihr alle drosselt. Eine Drosselung nach 10 Gigabyte mag ok klingen, doch ich als Mensch der oft pendelt würde ich zum Beispiel gerne in Remote-Desktop-Sessions arbeiten, ohne danach auf das Trafficniveau meines Geburtsjahres gedrosselt zu werden. Nun ist es ja so, dass in den meisten Verträgen steht, dass die Verfügbarkeit von Hochgeschwindigkeitsinternet keineswegs gesichert ist. Technische Gründe, sowie lokale Überlastungen, können immer entstehen, die Verfügbarkeit des Notrufs muss sichergestellt werden, und sicherlich lohnt sich Ihr Geschäft nicht ohne Overcommitting. Dafür habe ich (eigentlich kein, aber ich will mal nicht so sein) Verständnis.

Ich kann mir allerdings nicht vorstellen, dass der Traffichunger in Zukunft abnehmen wird. Was ich mir dementsprechend wünschen würde, wäre ein Tarif nach Vorrang-Modell: Für eine bestimmte Datenmenge (10GB scheinen momentan der Standard zu sein) hat man Vorrang, wie bisher auch, und erhält im Rahmen der technischen Möglichkeiten die hohen Geschwindigkeiten. Danach kann man, wie jetzt ebenfalls, gedrosselt werden (aber vielleicht nicht gleich auf 32k, wenn das möglich wäre, sondern auf irgendwas, mit dem zumindest einfache Dinge noch funktionieren – aber das nur am Rande). Allerdings wird man nur soweit gedrosselt, wie es notwendig ist, um den Kunden mit Vorrang ihr schnelleres Internet zu ermöglichen. Sollte sich also Beispielsweise in einer Funkzelle nur eine Person befinden, so bekommt diese die volle Geschwindigkeit trotz Trafficverbrauch. Nun bin ich technisch nicht hinreichend informiert um sagen zu können, ob dies wirklich ins Gewicht fällt, aber ich würde einfach mal ins Blaue vermuten, dass gewisse ungenutzte Reserven vorhanden sind. Ich persönlich wäre durchaus bereit, einen gewissen realistischen Aufpreis für so einen Service zu zahlen, und ich bin sicher, dass es einen Markt dafür gäbe. Das Fehlen echter Flatrates im mobilen Bereich ist für mich ein großes Manko.

Using state monads works well with Haskell, but as soon as you try to actually verify your software, it gets a lot harder. I am a fan of uniqueness types – they fit well into the framework of MLTT, and can be statically checked. Idris has experimental support. However, it can be undesirable to have purely syntactical extensions that lie outside of the scope of the type system. Extending the type system is possible but not the method of choice – in my opinion, the type system should be as simple as possible.

DiffArrays follow a different pattern: They are destructively modified in the backend, but their interface is referentially transparent: Old versions of the destructively modified array can be recreated. In theory, the overhead is limited to changing an old reference, as long as the array is used in a linear fashion. Native Coq uses them. Their definition is:

type 'a t = ('a kind) ref
and 'a kind =
  | Array of 'a array 
  | Updated of int * 'a * 'a t

That is, a diffarray is a (mutable) reference to an object that is either an array, or a key-value-diffarray-triple. Changing the value of an index in a diffarray "feels" like creating a modified copy of it. As soon as an old version of the array is modified, the array is copied; in this case, the algorithm will be slow.

There is a canonical equivalence relation between two diffarrays, namely the one that relates diffarrays which map the same key-value-pairs. As long as we are only using the interface for creating modified pseudo-copies of an array and reading its elements, there is no way to distinguish between arrays that are equal modulo this relation. If we forget for a moment that every diffarray is a mutable reference that points to an array or another such reference, we get the following algebraic definition of diffarrays:

Looking up the nth element would become

The equivalence would become . Any function that only uses our defined lookup function to access our array structure cannot distinguish equivalent diffarrays. We could as well work with . Especially, we could even replace an occurence of one representation of an array by another one, without significantly changing that term's behavior – but replacing one term with another is the same as destructively modifying a reference. And that is exactly what a diffarray is: Destructively modifying parts of terms, but in a way that cannot change the term's behavior.

And I assume that most uses of Haskell's unsafePerformIO are of this kind: They implement some stateful operation, but encapsulate it into a referentially transparent interface that makes different states indistinguishable.

Maybe by using the above construction, it would be possible to encapsulate some of such use cases into a dependently typed framework. Maybe in the form of quotient types, or in the form of higher inductive types.

Update: There appears to be a paper about basically the same thing. It might be even more useful than I thought, persistent arrays can be implemented better with mutable state. And furthermore, I was thinking about how this kind of thing could be used for memoization. I think it is undoubtedly useful.

Proofcheckers can be used to verify the correctness of proofs, which - in turn - can prove the correctness of programs. In theory. In practice, there is a slight problem: All of the modern proofcheckers are implemented in some high-level functional language, and their runtimes tend to be rather complicated. And they are not verified themselves.

There is the common concept of the "trusted codebase": You have to start with something, and the trusted codebase is the amount of program code you have to trust. Unfortunately, trying to keep the trusted codebase small while keeping proofs simple are contrary goals.

Coq addresses this problem by having a small kernel that checks the proofs, and lots of unverified code that produces proofs. This way, proving even complicated theorems becomes bearable. However, this can also result in regressions with newer versions of Coq: Tactics might do things differently in different versions, and automatic variable names might change. The common solution is to try to write proofs that do not depend on those names, or at least explicitly give these names. It is, however, not always possible. In theory, it is possible to export the proofs into a common format which is (mostly) version independent, but doing that is like saving compiled libraries to prevent compiler incompatibilities: Specifications tend to change, and proofs should therefore be maintainable, and maintainable proofs can always be ported to newer versions of Coq.

The situation is not perfect, but at least, no false proofs are accepted - mostly. There have been bugs that allow deriving False, and therefore everything else. This is a common criticism of program verification - how trustworthy can an unsound proofchecker be? But think about what we are actually talking about: People have written an algorithm, have thought about an informal proof ("proof in words") that would otherwise be accepted, and then formalized it for a proofchecker that has a bug which is usually some exploit of an edge case. I think a scenario where this actually leads to a bug in the resulting program code is highly unlikely. I wonder if something like that ever even occured. I think, in conclusion one can say, a verified implementation is usually formally correct, and it is almost impossible for it to not satisfy the specification. And, above all, you do not lose anything: You will have to write code anyway, the process of verifying it will not introduce additional bugs.

That being said, it is – of course – very desirable to have a correct proofchecker. Ideally, it should be metacircular. To make it less prone to bugs, it is desirable to keep it as simple as possible. I tried to implement a simple proofchecker several times, but I always failed because at some point I didn't find it sufficiently simple anymore. In a functional language with algebraic types and automatic garbage collection, it might not be too hard — but also not elementary. OCaml, Standard ML and Haskell have sophisticated runtimes which might be a good thing when writing unverified high-level code, but for my taste, it is rather complicated for a proof checker. So I was thinking about what is needed to write a realistic proof checker.

I think, in the current situation, it is unrealistic to go to a lower abstraction level than C: C is the lingua franca. However, it is probably a good idea not to use C as a "portable assembler", but rather have a clean and obvious programming style rather than focussing on efficiency.

One reasonable way of encoding the several recursive definitions is using structs, unions and enums. It is probably the easiest way, but probably not the most efficient representation, but it should be portable and the resulting code should be readable. However, this results in complicated memory management. Any implementation would probably have lots of allocations of small structs that point to each other. Allocating objects can be done with malloc(3), but usually, malloc(3) is not meant to manage many small objects. A slice allocator on top of malloc(3) would solve that problem. But then again, malloc(3) bases on mmap(2). It would also make the implementation more complex.

Allocating and deallocating objects can be done directly in the code, but as this is done frequently, it is probably not a good idea to always do this explicitly. A copying garbage collector would probably be the best for this situation, and a simple copying garbage collector is probably bearable – however, it would increase the trusted codebase. Using a reference counter would also be sufficient, and one could simplify it a lot using __attribute__((__cleanup__())) from GCC. Still, all of those possibilities – including manual memory management – are rather complicated

The question is whether deallocating objects at all is necessary. As The Old New Thing points out, the null garbage collector is correct. A proof checker gets axioms and already proved theorems, a conclusion and a proof as input, and its only objective is to check whether this proof is correct, and maybe return an error message that indicates the error. A simple stack-oriented language that is sent through stdio should be sufficient, and therefore, it might be sufficient to never actually deallocate. This would be the UNIX way, probably: Do one thing and do it right. If it occurs that not enough memory is available for some proof, one could preload libgc.

At some point, the question is whether all of this is worthwile at all. One could just use C++ and std::shared_ptr and be happy. But then, the additional complexity of the C++ runtime arises. Well, LEAN appears to be written in C++, but I don't know about its memory management.

To this point, it is questionable whether it is really worthwile to try to write a typechecker only using low-level programming techniques, rather than relying on well-tested abstractions. Besides the already mentioned small likelihood of a critical bug in typecheckers that leads to wrong proofs of algorithms, even in the presence of such a bug, it would only have to be fixed once, so after 30 years without critical bugs, one could be pretty sure that everything works fine.

Of course, this is not the only reason for wanting an implementation of a proof checker in C. All the Systems appear to try to create an own programming language. I would rather like to have a library which I can use in the language of my choice. On the other hand, Coq has a way of calling external programs to provide proofs, which is in many cases equivalent to such a library.

External Content not shown. Further Information.

Die Deutschen™ wollen mehr Mitspracherecht der Bürger in der Wissenschaft.

Und wer sollte die Forschungs-Milliarden für diese Projekte verteilen? Das sollten „die Bürger“ entscheiden, ist mit 42 Prozent die häufigste Antwort.

Die selben Bürger, die dafür gesorgt haben, dass man in Deutschland kein Humaninsulin herstellen durfte? Die selben Bürger, die demokratisch einen Atomausstieg, einen Atomausstiegausstieg und einen Atomausstiegausstiegausstieg innerhalb von 20 Jahren gewählt haben? Die selben Bürger, die ihre Kinder zu Masernparties mitnehmen, und angst vor Strichcodes haben?

Die wollen jetzt darüber entscheiden, wie man am besten Geld für Wissenschaft investiert?

External Content not shown. Further Information.

The day I began writing this post was one of those rare days when I watched TV. Passively of course. It was about worried parents, and experts™ who fear that smartphones might be dangerous for children. I remembered that in bavarian schools, smartphones are forbidden. When I was a young child, people were worried that cartoon violence could make children violent. Then they were worried that video games were addictive and would harm children. Then computers and instant messaging. Well, we all exist. And most of us only suffer moderately.

It might be that some children actually had problems due to trends and technology. It might even be severe damage. Progress takes its toll. But on the whole, progress has improved and saved life, and it will probably continue. Probably we should, instead of blocking progress, try to be less of an asshole society, and actually help and support the people who had bad luck.

Some people might think that the use of modern technology is a way youth wants to set itself apart. But remembering my childhood, children rarely tried to keep it a secret: We always wanted to talk to grown-ups about the games we played, about the cartoons we saw, &c – they were just not interested. Maybe it would be the best for the children to actually care about what they do – even though it may not be interesting by itself. And by caring I mean really trying to understand it, not only half-heartedly worrying how it could possibly harm them. It is the world in which your children live, and that alone should make it interesting as a parent. If you are not willing to do that, do yourself and your would-be children a favor and just do not become a parent.

The world wants to boycott Germany? Or at least say so? Well, apparently they want to boycott buying German products, not getting German money.

It is easy to blame someone, especially someone with a history as bad as us Germans'. What I saw in this report about the poor Greeks' situation (having to give their children away) shocked me. And while there might be nationalism in Germany, most Germans would not agree to measures that lead to something like that. They just don't know that it is really that bad.

Don't forget: Many Germans are poor too - mostly not that poor apparently, but still poor. And their only daily lecture is Bild - which tells them that the lazy Greek people take away their money. The reason that poor Greek people are angry about Germany is similar to the reason that poor German people are angry about Greece: They think that it causes their bad situation.

So just today I read that Apple could have bailed out Greece twice. And I wonder: Why not #boycottApple then? But again, it is not Apple alone. I am sure there are many companies that could do so. And I am sure that there are many companies that even caused Greece's situation. Why don't we all just boycott them? Why not #boycottCapitalism?

Could it be because we all secretly love the current kind of capitalism? Greece benefited from it in the past, as well as Germany did. As Volker Pispers points out: It is the modern religion, you don't have to understand it, you just have to believe it.

While I can pity single persons, I do not pity the Greece people on the whole. For decades they accepted this system. And when it was too late, they elected extremist parties. I am sure if it was the other way around, they would have a government that would behave like Germany does now, maybe a little better, maybe a little worse.

And I am sure the day will come for many of the German people who cry about our precious German money being given away to greedy Greeks to be in need of help themselves. Hopefully the system has changed till then.

Every nation gets the government it deserves. (Joseph de Maistre)

External Content not shown. Further Information.

I am not a professional software developer — well, I guess in some sense I am, but at least not an industrial professional software developer. But at least what I heard from some industrial software developers, what I will describe now is a usual experience:

You develop a complex piece of software. Especially the "practical" pieces of software are usually evolutionally grown and very complex. And usually, when writing code, you write something very specific and nontrivial – because if it was trivial, there would usually be no reason to write it, except exercising, which is also pointless if the solution is trivial to you.

So what happens to me often (and as far as I heard, I am not alone with this) is that I wrote a large piece of software, and then compile and test it – just to eliminate the worst bugs and lots of small mistakes. I really hate this phase of writing code.

So recently, I had to optimize a functional algorithm. I did so, and it was really hard, it took me a few hours. Then I leaned back and had this feeling that I always have before the first debugging phase.

But just a few moments later I remembered: The code I have written was functional for a reason: The entire algorithm was formally verified against a specification which I already had debugged and reviewed thoroughly. Admittedly it took me longer to write verified code than it would have taken to write unverified code, but the whole phase of testing and debugging is practically nonexistent.

Induction is one of the nightmares of many computer science students, it seems. For mathematicians, it is a very natural concept, and often the first higher proof strategy. Induction itself is not hard, the problem is that most proofs involve a lot more work than just induction, and it can be hard to even find the right parameters for induction.

When doing type theory, one quickly notices that induction is somehow equivalent to recursion: Recursion operators have a type signature similar to the formulas which encode induction principles. This is not a coincidence - but recursion operators are not really intuitive either, for a beginner. However, I think that for many beginners who have at least a little knowledge about programming, the key for understanding induction could be recursion. Even though from a purely "practical" viewpoint, recursion might not be good programming practice (especially if you ask older programmers), it is a well-understood concept.

I assume that the reader knows what a function - in the sense of programming - is. I will use C notation here, but without pointer magic, to make it easily understandable.

A well known function is the factorial of a number. Mathematical notation for the factorial of is usually . For , we can "define" the factorial as . Furthermore, it is defined that . A simple implementation of this function in C would look like

int fact(int n) {
    int ret = 1;
    for (int i = 1; i <= n; i++) {
        ret = ret * i;
    }
    return ret;
}

And in fact, this would calculate the factorial (and is probably the way most software engineers would recommend). On the other hand, notice that for . This equation and fully determine the values of the factorial function. So, an alternative way to write a factorial function in C is

int fact (int n) {
    if (n == 0) return 1;
    else return n * fact(n - 1);
}

This function calls itself. This is called recursion, the function is called recursive. Notice that the function argument decreases. Behind this lies a simple principle: We can already calculate the function for a smaller argument, and we can use this value to calculate the function's value for the larger argument. We can reduce the problem to a simpler problem.

Another classical example for recursion (and especially for the problems with recursion) is the Fibonacci sequence. We define and for . This is a recursive definition. In C, we can write

int fib (int n) {
    if (n < 3) {
         return 1;
    } else {
        return fib(n-1) + fib(n-2)
    }
}

This definition has a major disadvantage: Its runtime is exponential (if you don't know what that means: really really slow). But it also has a great advantage: It is easy to write and easy to understand. The non-recursive definition looks like

int fib (int n) {
    int j = 1, k = 1;
    for (int i = 3; i <= n; i++) {
        int l = j + k;
        j = k;
        k = l;
    }
    return k;
}

This function is (arguably) harder to understand. This is often the case, and this is a common problem that computer science tries to solve: Things which are easy for humans are hard for computers and vice versa. That is why modern programming languages have abstractions like functions, classes, modules, etc. The art of computer science is to find a common language that both computers and humans understand well. For the hardest parts, people rely on mathematical proofs.

And one principle that makes it easier for humans to reason is to reduce a problem on simpler problems. And this is what recursion can do.

Now back to induction. The classical introduction to induction usually contains Gaussian sums: Assume we want to add the numbers from to , that is, we want to calculate . This is similar to the factorial, except that we use addition instead of multiplication. And of course, we can use the same function as above, and just replace multiplications with additions (and 1 with 0):

int gauss (int n) {
    if (n == 0) return 0;
    else return n + gauss(n - 1);
}

This function loops through all numbers below n, it takes linear time. This is not bad, but there is an easier way:

int gauss (int n) {
    return (n * (n + 1))/2;
}

In fact, for all . How do we know that this holds for every natural number? We can calculate this for every single number, but not for all numbers, as there are infinitely many natural numbers: We need a mathematical proof.

Before we go into induction, let us define a function from natural numbers to proofs. It is possible to do this formally, but not without a deeper understanding of mathematical logic - so we just do this informally here. Let us call this function . That is, is a proof for , is a proof for , and in general, is a proof for . We will define this function recursively.

For , we can just calculate this. So, we can say

.

For with , we can do recursion. proves that . Using this proof, we can set

We recursively defined a function that generates proofs. We did this in a very informal way, but with just a little more theory, we could do this in a fully formal way. (If you're interested, look at proof assistants like Coq or Agda.)

Denote by our proposition . Notice that is a proof of .

Notice that our definition of proves . Our definition of for the other cases uses - a proof of - to prove . So essentially, one could say that the recursive definition is itself a proof of . And notice that these are the premises of induction: If and for all we have , then we have for all .

There are more general induction schemes. For example, on binary trees, you can do induction on every branch - but the same way you can do recursion. The important part about induction (and recursion) is that something decreases, which cannot decrease infinitely often.