CS intro != Programming intro

Yes, "CS intro != Programming intro". Of course, it is not; maybe it would never occur to you that it could!? Well, in some places, though, the CS 101 ("introduction to CS") course ends up being essentially that, at least for some initial part. In some places (Koblenz included; see my OOPM course which is under attack in this post), the CS 101 course certainly ends up trying to also introduce the basics of programming (because the lecturer thought he/she should).

Here is why I think this is wrong and I apologize for coming forward so late:

  • Teaching the trivial level of programming ("getting you going with for-loops and such" :-)) just doesn't belong at the university. Maybe it never belonged there, but it certainly doesn't belong there anymore (for like 10-20 years) because it is just such a basic skill and there is so much guidance out there (Youtube etc.) that a contemporary student wanting to study CS must (or should) simply be beyond the point of needing such a trivial introduction.
  • At a "mediocre" university like mine (not overwhelmed exactly with brilliant students like this), we may get some otherwise possibly smart students however certainly lacking the most basic programming skills. Trying to get them up to speed in a university-style course is just frustrating everyone. It certainly has bored me near to death.
As a result, I am changing my CS 101 course (11 ECTS on paper, which is crazy in itself), per immediately (effective per end of October), as follows:
  • I decouple the objective of teaching basics of programming from other aspects of the course by running two tracks in parallel for some time. I collect these other aspects of the course, which are not about basics of actual programming, as the "theory track". The "programming track" is just there for those who need it. I expect it to be skipped by some students. The theory track will not make any assumptions about previous programming skills.
  • In the theory track, I spend several weeks overall on algebraic specification with applications to abstract data types and what is maybe best called "algebraically oriented domain modeling". See my recent slide deck (.pdf), in that instance Haskell-focused, though. This is joint work with Magne Haveraaen, University of Bergen. Welcome to the university! Students need to understand algebraic signatures and logic formulae. I am going to be nice with the students :-) So I shall limited coverage to pragmatic application of loose algebraic specifications; no term algebra, no quotient algebra, no Herbrand universe, no nothing. Structural induction is in, though! Sorry.
  • As the two tracks have progressed enough, synergy happens such that we implement specifications in Java or Python. Appropriate axioms from the algebraic specifications will lend themselves as assertions and as (parametrized) unit tests. We are also well equipped to discuss design by contract. We will also be prepared to appreciate the beauty (?) of UML class diagrams with OCL constraints. Algebraic specifications and logics are everywhere.
  • Logistically, I will be working mostly without slides. Rather I will use the whiteboard and different editors. The 101wiki of the 101companies project will host code and explanations and links to Wikipedia and other online resources. I will distribute some lectures notes, but no wall of text is going to replace my previous wall of slides. I want to get across (through focused lecture note material) some basic notions and for the rest I use online resources including commented specifications and programs as well as links to Wikipedia et al.
This gets us through 2/3 of the course. The remaining 1/3 of the course will use a single, sequential timeline. I will think about it, as it gets closer, but here are some thoughts:
  • Coverage of EBNF as another modeling method. Great! There is this wonderful connection between algebraic signatures and context-free grammars. Maybe, I will do term algebras anyway and manage to bore everyone to death.
  • Very basics of complexity theory. This can be done as soon as students are fluent in basic algorithmic programming. The same is true for the very basics of program verification. Coverage of program verification (Hoare logic) will definitely benefit from dealing with logic formulae in the theory track earlier.
  • There is a bunch of non-very basic programming topics that I tend to cover such as pointers, encapsulation, interfaces, modularity, inheritance, generics, exceptions. Some order needs to be determined. I have managed in the past.

Luckily, in the second semester, I teach "introduction to functional programming".  It is, of course, wonderful (in the view of the lecturer anyway) to make the students see the connection between algebraic specification and functional programming.


A tiny proof checker in Prolog

The Prolog code for this post is available on GitHub.

I am crazy enough to teach Hoare logic (axiomatic semantics) in the first course for our CS students. For instance, consider the following program (in some simple imperative language), which is supposed to compute quotient q and remainder r according to Euclidian division for operands x and y:

q = 0;
r = x;
while (r >= y) {
   r = r - y;
   q = q + 1; 

Given natural numbers x and y, the postcondition of the program is this:

x == q*y + r && q >= 0 && r>=0 && r < y

The precondition is this is:

x >= 0 && y > 0

We are supposed to prove the "triple" consisting of precondition, program, and postcondition.

Let's face it, verification according to Hoare logic is not easily understood by beginners. Many of my students aren't mathematically / logically fit, when they enter the curriculum. So it is a pain in the neck for them to listen and for me to present. However, I think it is still valuable to expose the students to Hoare logic early on, also in the hopes of related topics such as logics and verification to show up again later so that understanding arises through iterations.

So far I have avoided Hoare logic in my course on programming language theory, as I felt that operational and denotational semantics are more presentable in a programming-based fashion. That is, one can obviously write interpreters both in the operational and the denotational style, while the assumption is here that interpreters (say, programs) are easily digested by the average CS student as opposed to proofs and logics.

This time around, I am going to add axiomatic semantics to said course. To this end, I am presenting axiomatic semantics mainly through a simple proof checker that is developed in Prolog. (As reading material I recommend Chapter 6 of Hanne Riis Nielson, Flemming Nielson: Semantics with Applications: A Formal Introduction, Wiley, 1992 because it is easy enough and excellent overall and available online.) In this manner, the programmatic path is also exercised for axiomatic semantics. As a neat side effect, this also allows me to talk about concepts such as rewriting, normalization, simplification, again, in a programming-based fashion. (These concepts are close to my heart as a software language engineer and programming language researchers.)

Here is a quick look at the proof checker.

The rules of Hoare logic are (of course) represented as definite clauses. For example:

/* In the case of an assignment, its precondition is calculated from
 * its postcondition by substituting the LHS variable by the RHS
 * expression.

proof(P, assign(X, E), Q) :-
    subst(Q, X, E, P).

/* In the case of a statement sequence seq(S1, S2), the proof requires
 * subproofs for S1 and S2 subject to an intermediate assertion that
 * serves as postcondition of S1 and precondition of S2. To this end,
 * a statement sequence is represented here as a term with functor
 * seq_/3 (as opposed to the functor seq/2 of the original abstract
 * syntax) so that the extra intermediate assertion can be expressed.

proof(P, seq_(S1, R, S2), Q) :-
    proof(P, S1, R),
    proof(R, S2, Q).

/* In the case of a while-loop while(E, S), the precondition of the
 * loop is per definition the invariant I of the loop and the
 * postcondition must be equivalent to and(I, not(E)). A subproof is
 * due for the body S of the loop such that the invariant follows as
 * postcondition of S for the precondition and(I, E), i.e., the
 * invariant and the loop's condition hold at the beginning of the
 * execution of the body.

proof(I, while(E, S), Q) :-
    sameAs(and(I, not(E)), Q),
    proof(and(I, E), S, I).

/* The precondition of a proof can be strengthened. While
 * simplification/normalization of assertions is performed
 * automatically, strengthening must be explicitly requested. (This is
 * well in line with the usual extra rule of Hoare logic for
 * strengthening the precondition.) In the following notation, we
 * assume pseudo syntax to express the precondition before
 * strengthening, whereas the precondition of the triple is the
 * strengthened one.

proof(P, pre(R, S), Q) :-
    implies(P, R),
    proof(R, S, Q).

subst/4 is substitution of variables by expressions within assertions.
implies/2 is logical implication.
sameAs/2 is equivalence of assertions modulo normalization.
Some rewrite rules of normalization are included for illustration:

% Reflexivity
rewrite(eq(X, X), true).
rewrite(geq(X, X), true).

% Prefer right-associativity over left-associativity
rewrite(and(and(E1, E2), E3), and(E1, and(E2, E3))).
rewrite(or(or(E1, E2), E3), or(E1, or(E2, E3))).

% Unit laws
rewrite(and(true, E), E).
rewrite(and(E, true), E).
rewrite(or(false, E), E).
rewrite(or(E, false), E).
rewrite(add(number(0), X), X).
rewrite(add(X, number(0)), X).

Here is a simple (incomplete) axiomatization of implication:

% Implication complemented by normalization
implies(E1, E2) :-
    normalize(E1, E3),
    normalize(E2, E4),
    implies_(E3, E4).

% Search rules for implication
implies_(E, E).
implies_(_, true).
implies_(and(E1, E2), and(E3, E4)) :-
    implies_(E1, E3),
    implies_(E2, E4).
implies_(and(E1, _), E2) :-
    implies_(E1, E2).
implies_(and(_, E1), E2) :-
    implies_(E1, E2).
implies_(greater(X, number(N1)), greater(X, number(N2))) :-
    N1 > N2.

Here is a simple test predicate for proving correctness of an if-statement:

% Proof for a simple if-statement that computes the max of a and b
prove_if :-
      greater(var(a), var(b)),
      pre(true, assign(r, var(a))),
      pre(true, assign(r, var(b)))
     or(eq(var(r), var(a)), eq(var(r), var(b)))

In abstract syntax, Euclidean division looks like this:

    assign(q, number(0)),   
      assign(r, var(x)),
        geq(var(r), var(y)),
          assign(r, sub(var(r), var(y))),
          assign(q, add(var(q), number(1)))))))

Here is the proof for Euclidian division; it contains the loop invariant and all other details of the proof.

% Proof for Euclidean division
prove_div :-

      % "As declared" precondition of the program
      % x >= 0 && y > 0
        geq(var(x), number(0)), % As computed
        greater(var(y), number(0))), % Vacuously added for division by zero

      % Strengthen precondition

        % Computed (weakest) precondition of the program
        geq(var(x), number(0)),

        % Beginning of program code

          % q = 0;
          assign(q, number(0)),   

          % Intermediate assertion
            eq(var(x), add(mul(var(q), var(y)), var(x))),
              geq(var(q), number(0)),
              geq(var(x), number(0)))),

            % r = x;
            assign(r, var(x)),
            % Intermediate assertion = invariant for while loop
              eq(var(x), add(mul(var(q), var(y)), var(r))),
                geq(var(q), number(0)),
                geq(var(r), number(0)))),

              % Loop condition                     
              geq(var(r), var(y)),
              % Strengthen precondition
                % Computed precondition of body
                  eq(var(x), add(mul(add(var(q), number(1)), var(y)), sub(var(r), var(y)))),
                    geq(add(var(q), number(1)), number(0)),
                    geq(sub(var(r), var(y)), number(0)))),
                % Loop body
                  % r = r - y;
                  assign(r, sub(var(r), var(y))),

                  % Intermediate assertion
                    eq(var(x), add(mul(add(var(q), number(1)), var(y)), var(r))),
                      geq(add(var(q), number(1)), number(0)),
                      geq(var(r), number(0)))),
                  % q = q + 1;
                  assign(q, add(var(q), number(1))))))))),

      % "As declared" postcondition of the program
      % x == q*y + r && q >= 0 && r>=0 && r < y
        eq(var(x), add(mul(var(q), var(y)), var(r))),
          geq(var(q), number(0)),
            geq(var(r), number(0)),
            not(geq(var(r), var(y))))))

It just works:

?- prove_div.


My Gear Fit Wish List

For like 10 days I own and use a Samsung Gear Fit.

I love it. I don't agree with this negative review.

However, I hope Samsung improves the software in a timely manner.

Here are some proposals, I should edit this blog post, as I see fit.

Bug report: Cycling exercise stops recording because of "no movements"

This happens after 10mins of recording. I think this happens because it uses a sanity check that may be right for running exercises, but there is no arm/hand movements, if you are cycling in a proper way. Within some time window, I can cancel the stop message to make it continue measuring. Anyway, this is highly annoying, as I need to hit a small on-display button while cycling. I don't see how one could not have caught this by basic field testing. [Added on 19 May 2014]

Feature request: Usable wake-up gesture needed

Currently, we have the choice between pushing the small hardware button on the Gear Fit to wake it up or relying on movement-based wakeup such that one lifts up the hand, as if one wanted to look at the display. The first option is clumsy, especially when you are doing sports. The second option is annoying because the display goes on all the time. Simple proposal: provide touch-based wakeup. Alternative: use a more unique movement pattern for wakeup. Some sort of shaking would also be conceivable. Combination of movement and touch Ok, too. [Added on 19 May 2014]

BTW, here is also a forum for the Gear Fit.



Einträge aus dem gefälschten Tagebuch eines Zonenprogrammierers um Weihnachten '88

Ralf Lämmel, 17.12.2013, Redevorlage für eine tierisch ernste Weihnachtsfeier


Derartige Text generieren mitunter gehässige Leserkommentare, welche dann hinterfragen, wie es sein kann, dass Beamte dieses Landes ihre Zeit auf solchen Quatsch verwenden. Deswegen soll hier ich pro forma betonen, dass ich diesen Unsinn zwischen den unbezahlten Überstunden an einem Wochenende durch grobe Vernachlässigung etwaig empfohlener Schlafmengen erstellt habe. Auch möchte ich erwähnen, dass ich als geborener Ostzonenprogrammierer ja nur durch geschichtliche Verwicklungen in diesem System gelandet bin, dessen Überlegenheit ich aber allein schon an der Menge und der Qualität der verfügbaren Bananen ablesen kann.

Wir versetzen uns zurück in das Jahr 1988, also dem Jahr vor 1989, also dem Jahr vor dem Jahr, in dem die Mauer viel -- wie man so sagt. Eigentlich ist die Mauer ja erst viel später vollständig weggetragen worden und bis dahin standen durchaus noch diverse Mauerteile; sie lagen also nicht rum bzw. sie waren nicht schlagartig umgefallen; auch waren sie nicht alle umgefallen worden. So einfach lies sich diese Mauer nicht fällen bzw. umwerfen.

Es ist Weihnachten 1988.

Ein gewisser Gefreiter der Reserve, Ralf Lämmel, geboren in Korl-Morx-Stodt (der Stadt mit den drei “Os”), aufgewachsen in Rostock, militarisiert in Stahnsdorf bei Potsdam, zum Studium der Informatik nach Rostock zurückgekehrt, befindet sich im ersten Semester. Er hat aus unerfindlichen Gründen unlängst und angeblich begonnen, ein Tagebuch zu führen. Hierzu sei erwähnt, dass es zwar keinen Strom und keine Bananen in der Zone gab, aber Papier und Bleistifte waren rationiert verfügbar für politisch konforme Staatsbürger. Im folgenden erlangen wir empirischen Einblicke in die ostzonale Programmiererpsyche durch die Betrachtung ausgewählter Tagebucheinträge um eben Weihnachten 1988 herum.


Sonntag, 18.12.1988

Der Meli-Club gestern war einfach cool. Meine Freundin schaute gut aus. Auch habe ich ein neues Getränk entdeckt -- so ein Wermut, der sich Gotano schimpft. Damit entsage ich “Dozentenblut” und “Bretterknaller”. Es ist so schade, dass ich nicht auch donnerstags im Meli-Club sein kein, aber die Vorlesung “Dialektischer Historischer Materialismus” beginnt schon 7:15 Uhr am Freitag. Es gibt wohl eine Hausarbeitsoption für das Fach. Damit könnte ich donnerstags auch in den Meli-Club gehen -- so wie es für meine Freundin und die anderen Grundschulpädagoginnen kein Problem ist.

In dem synaptisch erweiterten Zustand des Gotanogenusses beschlossen XYZ (Name geschwärzt) und ich, eine Forschungsidee im Kontext natürlicher Sprachverarbeitung zu entwickeln. Dazu dachten wir zunächst tiefgründig über den gerade hörbaren Text von Marianne Rosenberg’s "Er gehört zu mir" nach, welcher zu einem Meli-Club-Abend so gehört wie der Name an der Tür.

Erste Strophe von Marianne Rosenberg’s “Er gehört zu mir”:

Er gehört zu mir, wie mein Name an der Tür,
und ich weiß, er bleibt hier,
nie vergeß ich unseren ersten Tag,
Naaa naa naa na, na na na
denn ich fühlte gleich, daß er mich mag,
Naaa naa naa na, na na na
ist es wahre Liebe (uuuhhhuuuhhuuu)
die nie mehr vergeht (uhuuuhuu)
oder wird die Liebe, vom Winde verweht?

Wir definierten folgende Forschungsfragen, welche durch eine Analyse mittels natürlicher Sprachverarbeitung bzw. Corpusstudien auch unter Einbezug sozialistischen Liedgutes zu adressieren wären. Auf jeden Fall würde Prolog in diesem Projekt zum Einsatz kommen.


  1. Gibt es charakteristische Elemente in diesem Text, welche dieses Lied als eine Ausgeburt des Klassenfeindes entlarven? Ist dies vielmehr ein unentscheidbares Problem bzw. ein Problem, was nur durch die sogenannte "starke Artificial Intelligence" gelöst werden kann?
  2. Welche subliminalen Elemente führen zu der mysteriösen Massenpsychose in dem sozialistisch geprägten Studentenclub so dass sich politisch gebildete Studierende und andere sozialistische Persönlichkeiten diesem imperialistischen Gedankengut zuwenden?
  3. Ist Marianne Rosenberg eventuell dann doch verkappt revolutionär?
  4. Liefert der Text einen Beleg für die imperialistisch etablierte Verhaustierung von Mãnnern?

Ultimativ führte das Lied uns gegen Ende des Abends, also am frühen Morgen, zu allgemeinen Reflektionen über unser beginnendes Informatikstudium und das Leben an sich:

Weitere Fragen:

  1. Warum müssen wir in Pascal und C programmieren? Diese Sprachen sind doch ganz offensichtlich ungeeignet, um einen klaren Gedanken zu fassen? Kann die sozialistische Gesellschaft auf Dauer erfolgreich sein, wenn sie solche degenerierten (imperativen also imperialistischen) Sprachen favorisiert?
  2. Wie erklären wir unseren Freundinnen, was wir denken? Gibt es notfalls auch hinreichend gut aussehende Informatik-Studentinnen und hinreichend viele dergleichen? (Später zugefügte Anmerkung auf dem Rand des Tagebuches: Weitere empirische Untersuchungen suggerieren, dass Mathematikerinnen auch in den Suchraum aufgenommen werden sollten.)

Im Nachhall dieser Überlegungen habe ich gerade einen Brief an die Kreisleitung der SED gesendet, um die politische Integrität unserer Professoren überprüfen zu lassen hinsichtlich der systemfeindlichen Auswahl von Programmiersprachen im Curriculum.

Freitag, 23.12.1988

Ich wurde mit dem Weihnachtsgroßeinkauf beauftragt. Die Ente hat meine Mutter schon ergattert so dass nur noch Grundnahrungsmittel zu besorgen waren. Hier ist der Kassenzettel:

  • 100 Brötchen zu je 0,05 Mark, insgesamt 5,00 Mark
  • 7 Leckermäulchen zu je 1,00 Mark, insgesamt 7,00 Mark
  • 1kg Kaffee = 8 Packungen zu je 8,75 Mark, insgesamt 70 Mark
  • 10 Flaschen Club-Cola zu je 0,42 Mark, insgesamt 4,20 Mark
  • 1 Schlager-Süßtafel zu 0,80 Mark
  • usw.

(Siehe weitere Preisbeispiele aus der DDR.)

Kaum bin ich zuhause, sehen wir unter auf der Strasse jemand mit Orangen. Ich mache mich dementsprechend wieder auf den Weg in die Kaufhalle. Solche Schnelligkeit zahlt sich aus. Man hat mir dann 1kg Orangen verkauft; mehr gab es nicht pro Person.

Schliesslich durfte ich noch in das Kaufhaus eilen, um ein paar Jahresendflügelfiguren als Schmuck für den Endjahresbaum zu kaufen sowie ein paar Endjahrespuppen ohne Flügel aber mit Mütze und Bart und aus Schokolade -- also zum Verzehr bestimmt.

Montag, 26.12.1988

Das ist ein ganz besonders schrecklicher Montag: Rechenzentrum geschlossen, Freundin bei den Eltern, Alternativen nicht zugreifbar bei geschlossenem Meli-Club, polnische Flugente zu trocken, Orangen ungeniessbar. 

Die Kuba-Orangen sahen lecker grün aus in der Kaufhalle, aber die Drängelei, das Anstehen und das viele Geld waren es nicht wert; die Orangen sind voll mit Kernen und total sauer. Vielleicht ist etwas dran an dem Gerücht, dass die Kuba-Orangen Fidel Castro's Rache sind.

Auch politisch fühle mich ein wenig alleingelassen. Wie war es doch noch schön, als wir bei der Fahne im Verband der Kompanieeinheit ab und an den “Roten Montag” hatten, der uns für das Vaterland mobilisierte. In dieser Situation der totalen Trostlosigkeit verliere ich mich versehentlich beim Westfernsehen. Das ist aber voller Lügen. Die lassen es so ausschauen, als wenn es dort leckere Orangen und Bananen gibt. Die Wahrheit sieht anders aus, wie wir es aus der NVA-Bibel "Vom Sinn des Soldatseins" wissen (Seite 35 in der mir vorliegenden Version):

“Den Lebensinteressen der Völker entgegen steht die Herrschaft des Imperialismus. Auf sein Konto kommen [...] Armut, chronische Unterernährung und hohe Kindersterblichkeit. Die Geschichte hat ihr Urteil über diese historisch überlebte und dem Untergang geweihte Gesellschaftsordnung längst gesprochen.”

Das zeigt doch ganz deutlich, dass es dort keine Orangen, keine Bananen oder sonstige vitaminreiche Kost geben kann. Ich danke Marx und Lenin, dass sie uns eine Alternative gebacken haben. Bei uns gibt immer leckere Äpfel und Möhren. Der Sozialismus hat den Skorbut besiegt.

Freitag, 30.12.1988

Es ist schon eine eindrucksvolle Koinzidenz, dass die aktuelle Hausaufgabe in der “Einführung in die Programmierung” die Warteschlange thematisiert, während Silvester vor der Tür steht und damit das alljährliche Ritual des Knallererwebs ansteht. Am Mittwoch habe ich mich ordentlich gegen 23 Uhr an die Warteschlage angehängt. Das war zu spät! Das Kontingent an Knallern war 42 Minuten nach Ladenöffnung, also um genau 9:42 Uhr erschöpft. Zu diesem Zeitpunkt konnte ich die Ladentür nur nicht einmal sehen.

Allerdings war die Zeit in der Schlange nicht ganz vergebens. Ein Thema in meinem Schlangensegment war die prekäre Wohnungsfrage. Es scheint immer noch geltende Praxis zu sein, dass man entweder bis etwa zum Alter von 30 Jahren bei Muttern leben soll oder man heiraten und ein Kind kriegen soll, um eine Wohnung zu bekommen.

Allerdings scheint das bald besser zu werden. Ein netter Parteifreund konnte mit einem Zitat aus Erich Honecker’s Autobiographie “Aus meinem Leben”  aufwarten (Seite 304 in der mir vorliegenden Version):

“Unser Zentralkommitee beschloß im Oktober 1973 ein Wohnungsbauprogramm, um bis 1990 in der DDR die Wohnungsfrage als soziales Problem zu lösen.”

Sobald meine Freundin wieder vor Ort ist, werde ich ihr mein Aktvitätsdiagramm zur Lösung unserer persönlichen Wohnungsfrage demonstrieren. Das Diagramm enthält ein Fork/Join zur Maximierung der Optionen zum Erhalt einer Wohnung. In einem der parallelen Abläufe vertrauen wir auf Erich's Versprechen und hätten damit spätestens am 31.12.1990 eine Wohnung ohne weiteren physischen Aufwand. Parallel könnten wir aufgrund gesunden Misstrauens auch ein Kind in die Welt setzen und damit eventuell schon im Herbst 1989 eine Wohnung zugewiesen bekommen. Das Diagramm ist in Prolog ausführbar. 

Es bleibt zu hoffen, dass die Betonklötze von Professoren nicht doch wieder ihr C-ähnlichen Gebrechen zur Lösung derartiger Probleme pushen. Nicht alle Professoren sind aber so reaktionär. Prof. XYZ  (Name geschwärzt) hat unlängst von der Sprache Hope erzählt und ich habe noch nie soviel Hoffnung verspürt. Die funktionale Programmiersprache Hope kann Funktionen höherer Ordnung gut ausdrücken, Fallunterscheidungen über Datenmustern beschreiben und sie ist stark getypt. Ich werde meine Westverwandten antickern, mir mehr Informationen dazu zu besorgen. Hope soll bald zu mir gehören, wie die Türklinke zur Tür.


Wer etwas Ernsthaftes über die Geschichte der Informatik in der DDR lesen möchte, dem sei der Artikel Integration der Informatik-Standorte der DDR in den Fakultätentag empfohlen.


Install Mac OS X Mavericks from USB

It's really easy.

Why would you do it?

  1. Do it on many machines without downloading Mavericks time and again.
  2. Do it on a machine that it not working proper in terms of its Mac OS X install.
  3. Do it on a machine where you want to flatten the old Mac OS X.
  4. Do it on a machine that refuses to install in the normal way so that you like to flatten.
For instance, I had a 10.6 machine where the installer would fail because the existing partition was found to be non-usable. Apparently, this is a common problem also covered by the Apple KB. My partition was a standard one, as far as I can tell.

How to prepare a USB install drive?

A somewhat verbose story is given elsewhere:

If you know sudo, then it is trivial:
  1. Format the USB stick with Disc Utility; call it "Untitled" say.
  2. Just download Maverick (as if you wanted to install it).
  3. Run the following sudo command that prepares the USB drive in a few minutes.
sudo /Applications/Install\ OS\ X\ Mavericks.app/Contents/Resources/createinstallmedia --volume /Volumes/Untitled --applicationpath /Applications/Install\ OS\ X\ Mavericks.app --nointeraction

So basically, the installer has this great API to create an install drive!

How to install from the USB drive?

  1. Insert the USB drive into the computer.
  2. Boot and press "option" to see the list of boot devices.
  3. Select the USB drive.
This would launch the installer.

How to reset and install?

If you want to run disk utilities (in order to flatten the previous system), press the "R" key right after having selected the USB drive. This would start the recovery partition on the USB drive, which gives you access to the disk utilities. In this manner, you can, for example, format the old drive and thus prepare for a fresh install of Mavericks leaving the past behind.


With two friends, I participated in a "Dinner for one" online quiz last night.

Quite proud of our combined insight.

Urkunde: Auswertung für den Test
Dinner for one
Super! Sie wissen was Miss Sophie und James jedes Jahr tun!

Sie haben 10 von 10 Aufgaben richtig beantwortet.
Im Durchschnitt haben die 1912 Surfer, die das Quiz gemacht haben, 6.77 richtige Antworten gegeben.
Auch das Quiz Dinner for one spielen?


Undergraduate reading material on SLE

What is SLE?
You can shop around for definition attempts.
... on the websites of SLE conference series.
... in the guest editors' introduction to the IEEE TOSEM 2009 special issue on SLE.

As a matter of fact, we don't have a proper, generally accepted and adopted definition.
This indeed also showed at last year's SLEBOK workshop at SLE 2012.
There is quite a few people (including me) who think that this needs to be fixed.

On a related account, it is not even particularly clear what the core or extended set of SLE concepts would be. This makes it hard to properly cover the subject in teaching. I somehow have managed in my SLE class, but I do not claim to be very consistent and palatable as to the use of terminology (ontology) in the course.

This semester's edition of my SLE course will feature reading (and corresponding presentations and discussions by the students) with one reading slot focused on basic SLE literature. I have started to collect a richly annotated bibliography of "fundamental SLE papers", which I released at OOPSLE 2013 (at WCRE 2013) in Koblenz earlier this week.

Please have a look:

I hope it may be useful for others. 
I also look forward collaboration on the subject.