kirjoittaessani

Schlagwort: Programmieren

  • Visited

    It has taken me some time, but I have pushed my lox-spark project one step further: the code is now complete up to the end of chapter 5 in Bob’s book.

    Why has this taken so long, even though the new code is still unproven (i.e. the proof hasn’t progressed beyond chapter 4)?

    The Visitor pattern turned out to be quite​ a nut to crack. Bob has used templated accept() methods. This means a concrete visitor can choose to return whatever type it needs — the example AST printer returns a string, but later in the book, other types might come in handy. Unfortunately, in Ada generic functions cannot be overloaded, so I couldn’t copy this approach. I tried to code around this restriction only to discover I didn’t really understand the Visitor pattern (which I hadn’t encountered before).

    After some searching, I found an Ada implementation by Matthew Heaney. He, too​, uses generics, but in a different way. The gist is that instead of returning a value, the Visitor type („object“) stores the data internally — this is not a problem because the abstract visitor type is extended (subclassed) anyway — and can then be queried by the caller. There seems to be a bit more boilerplate code, but most of this is written by Lox’s source code generator, so this is no real problem.

    The second nut stems from a shortcoming in current prover technology: Gnatprove cannot deal with aliasing (i.e. writing to one variable changes the value of another), and therefore access variables (pointers) are not allowed in SPARK. This is not as large a problem as it may seem since Ada programmers use access variables very sparingly. But the abstract syntax tree has nodes containing other nodes, so some kind of reference is needed.

    I have decided to store all Exprs in a Formal_Indefinite_Vector (a container supplied by the standard library) and refer to them by their index in the vector.

    I am quite satisfied with how far lox-spark has come, this is a good way to start the weekend.

    What’s next? Obviously, the new code needs to be annotated and proven. Also, chapter six has been out for almost two weeks, so there’s still more code to be written. I haven’t yet decided on where to start, so maybe I’ll take advantage of git and do both in parallel.

  • Generation Lox

    My current pet project is coming along quite well: the implementation is complete up to chapter four (Scanning). More importantly, the AoRTE proof (absence of runtime errors) is also completely done. The only shortcomings are a handful of package bodies that are compiled with SPARK_mode => off: Ada.Command_Line and SPARK.Text_IO come to mind.

    A few days ago, Bob has published the fifth chapter of his book. It is mainly about theory, and the only code it contains is a tool that generates source code for a part of the interpreter (the type hierarchy of the abstract syntax tree).

    I thought about this for a while, and came to the conclusion I would not follow his path. Instead, I planned to write the types by hand. Here is why: generating source code is not really a problem, and since the generator would not be part of the final program, I would write it in plain Ada (without proving anything). The resulting code, however, would be part of the interpreter and thus needs to be proven. I could add the necessary annotations by hand, but that would defeat a big advantage of the generator: one can make changes at a high level (namely, change the input to the generator) and regenerate the sources. This is fine for ordinary languages, but it will kill my hand-written annotations.

    Meanwhile, about a dozen Lox ports have appeared on github. I looked at all those I could find, but nobody seems to have written code related to the new chapter. Either the other developers have not yet found the time to implement the generator, or they, too, have their doubts.

    Somehow, this lack of activity has prompted me to revise my decision: I will implement the generator, and I will generate annotations as well. After all, this project was meant to help me learn something new, and to be a challenge. But what good is a challenge unless it is challenging?

    This should keep me busy in the coming days (I have not yet written any code for the generator). A quick Google search tells me that I can build multiple executables from the same project with GNAT, so that simplifies things on the organisational side.

    Watch this site (or better yet, github) for updates!

  • Sparkling Lox

    For some time, I’ve taken an interest in software engineering. With that, I mean robust software. After learning about Ada (my first project is from 2011), I haven’t looked back (at C/C++, that is); Since then, I’ve learned a little about formal methods. So far, a few half-hearted attempts at SPARK/Ada have been the only results.

    Now, I have stumbled across a project of Bob Nystrom’s: He has designed a simple programming language, Lox, and is writing (and continuously publishing) a book on how to implement it. He has chosen Java and C, but quite a few folks have taken his code and re-implemented it in various languages: Alejandro Martinez (Swift), Ivan Katanic (C++), Paul Jackson (Go), Sasha Matijasic (Python).

    So, why not do a SPARK port? I have some past experience with various parsers, so writing the bare code should not be that hard. Once that is done, annotations could be added and proofs done. The advantage of this project is that Bob is doing it now, chapter by chapter; I expect to follow at more or less the same pace, so if SPARKifying means I have to change something fundamental, I do not have to do that to the complete program. Instead, I can deal with problems as they crop up in the early stages.

    I should add that SPARK can be used in different ways (or maybe I should say intensities). In the simplest case, only absence of runtime errors is proven. However, it is also possible to prove functional correctness at various levels: For example, one might set out to prove that a sorting subroutine actually returns a sorted list. This approach can be extended to more and more routines and eventually encompass the whole program. I do not know how far down this path I will (manage to) go, and in any case I have no idea how to prove functional correctness for a compiler.

    Time will tell, I guess. Back to writing code now.

  • Lessons learned

    [lang_en]Actually, I have known this for some time, but today, it has bitten me again: Interpreted languages ((like Python)) are not suited for application development. Period. Use them for quick hacks, or for prototyping, or in lieu of a shell script. But never for real applications.

    People tend to say Computers are so fast today the overhead does not really matter, and if it does for a few inner loops, no problem: our language can interface with C. But that is beside the point. The real disadvantage of these languages is not their (somewhat inferior) execution speed, but their lack of static checking. If you write bogus in a compiled language, chances are the compiler will catch it. Some stricter languages ((like Ada)) will catch more kinds of bogus than more lenient ones ((like C)), but there are surprisingly many ways to write bogus that every compiler will catch. Interpreted languages do not have a compile phase, they just throw an exception when encountering bogus at runtime. If they encounter it: There are many execution paths through a program, and some may not be followed very often, making it easy to write, install, and use completely broken software. You may say Well, write tests then, but as useful tests are, they come with large disadvantages when relied upon as the only means of detecting errors: Firstly, they have to be written. A compiler knows about the language, but the developer has to write all necessary testcases by hand. It is easy to overlook something, and it is also very easy to be lazy and write too few tests (or none at all). Secondly, executing tests takes machine time (probably more than what was saved by not compiling), and writing tests takes developer time (lots of it). Finally, the static analysis a compiler provides tends to catch different errors than tests do, so combining the two will simply catch more problems than either method on its own.

    Oh, and then there is the problem of external code. Libraries, modules, whatever. APIs should not change (needlessly), but sometimes they do. With ordinary binary code, there is an established way to keep around different versions of a given library, so older programs using an older API can still function. I am not aware of a similar mechanism for Python, so getting ImportErrors from a module that installed just fine is not that unusual. In fact, implementing such a method for an interpreted language would be somewhat more involved than for a compiled one: When a programmer links to a shared library, the linker will take that to mean the latest installed version of that library. The version number is then encoded into the application binary, so the correct library will be used whenever the application is started. However, the very nature of an interpreted language means that the program is not touched by anyone but the developer. So if the developer does not demand a particular version, nothing else does, either. Seriously: use a tool that fits the job rather than clutching a hammer and trying to see nails everywhere.[/lang_en]

    [lang_de]Eigentlich weiß ich das ja schon länger, aber heute ist es mir wieder schmerzhaft bewußt geworden: Interpretierte Sprachen ((z.B. Python)) sind zur Entwicklung ernsthafter Programme ungeeignet. Für Prototypen, einen schnellen Hack, oder als Shell-Skript-Ersatz sind sie eine feine Sache, aber nicht für echte Programme.

    Man hört oft, Computer sind heutzutage so schnell, daß das schlechtere Laufzeitverhalten nicht ins Gewicht fällt, und falls doch ein paar Stellen kritisch sind, so ist das auch kein Problem: die Sprache kann C-Routinen aufrufen. Aber darum geht es nicht. Die echten Nachteile liegen nicht in der Ausführungsgeschwindigkeit, sondern in der fehlenden statischen Prüfung des Codes. Wenn man in einer kompilierten Sprache Quatsch schreibt, dann kann man darauf hoffen, daß der Compiler das bemerkt. In manchen strengeren Sprachen ((z.B. Ada)) läßt der Compiler weniger Quatsch durchgehen als in nachgiebigeren ((z.B. C)), aber es gibt erstaunliche viele Sorten Quatsch, die jeder Compiler findet. Interpretierte Sprachen kennen keinen Compiler, deswegen finden sie den Quatsch erst zur Laufzeit. Wenn sie ihn finden: Es gibt viele Pfade durch ein Programm, und einige davon werden nur selten benutz; deshalb ist es einfach, völlig vergurkte Programme zu schreiben, zu installieren, und zu benutzen. Es heißt dann oft Deshalb brauchen wir Tests, aber so nützlich Tests auch sind, so haben sie doch gewichtige Nachteile (jedenfalls wenn sie die einzige Möglichkeit sind, Fehler zu finden: Zuerst müssen sie überhaupt geschrieben werden. Ein Compiler versteht die Sprache, aber der Entwickler muß alle nötigen Testcases von Hand schreiben. Dabei kann man leicht etwas übersehen, und noch leichter aus Bequemlichkeit zu wenige (oder gar keine) Tests schreiben. Zweitens braucht das Abarbeiten der Tests Rechenzeit — wahrscheinlich mehr, als man durch den fehlenden Compilerlauf gespart hat; und das Schreiben kosts Entwicklerzeit, und zwar eine Menge. Schließlich findet der Compiler oft einfach andere Fehler als Tests, und wenn man beides einsetzt, findet man mehr Fehler.

    Ja, und dann gibt es noch das Problem mit externem Code. Bibliotheken, Module, oder wie man ihn auch nennen will. APIs sollten sich nicht ändern (jedenfalls nicht ohne guten Grund), aber manchmal tun sie es eben doch. Für gewöhnliche, binäre Programme gibt es wohldefinierte Mechanismen, um verschiedene Versionen einer Bibliothek gleichzeitig vorzuhalten, damit ältere Programme immer noch laufen. Einen entsprechenden Mechanismus für Python kenne ich nicht, und so ungewöhnlich ist es nicht, wenn ein sauber installiertes Modul mit ImportErrors um sich wirft. Wenn man eine solche Methode entwickeln wollte, hätte man auch mit einem zusätzlichen Problem zu kämpfen: Wenn ein Programmierer eine shared library verlinkt, dann nimmt der Linker automatisch die neueste installierte Version dieser Bibliothek. Die Versionsnummer wird dann in dem kompilierten Programm verewigt, und wenn man es irgendwann später startet, wird die richtige Bibliothek benutzt. Es liegt aber gerade im Wesen einer interpretierten Sprache, daß der Programmcode nur vom Programmierer verändert wird. Wenn dieser also nicht von Hand eine bestimmte Bibliotheksversion anfordert, dann tut das auch keine andere Instanz.

    Im Ernst: man sollte Werkzeuge verwenden, die für die Aufgabe geeignet sind, anstatt sich verzweifelt an seinen Hammer zu klammern und überall Nägel zu sehen.[/lang_de]

  • Suboptimal

    Ja, da war ich wohl ein wenig voreilig, das Verständnis des Buildsystems anzunehmen. Das stellte sich heraus, als ich den erfolgreich kompilierten gcc unter einem Debugger ((Für den Fall, daß noch nicht alle des Programmierens nicht mächtigen Leser aufgegeben haben, sei gesagt: Ein Debugger ist ein Programm, mit dem man den Ablauf und den Zustand eines anderen — möglicherweise fehlerhaften — Programmen schrittweise verfolgen kann.)) betreiben wollte. Wer schon einmal versucht hat, ein Kompilat mit eingeschalteter Optimierung zu debuggen, weiß, was ich meine: Variablen lassen sich nicht mehr auslesen, das Programm scheint im Code wirr vor und zurück zu springen — selbst ein sehr einfaches, selbst geschriebenes Programm ist kaum noch nachvollziehbar. Nicht so schlimm, dachte ich mir, und habe mit CFLAGS='-g -O0' configure gleich den nächsten Build angestoßen. Die Ernüchterung folgte allerdings auf dem Fuße: ((Jedenfalls halbwegs — so ein Notebook ist nicht gerade die schnellste aller Entwicklungsmaschinen)) die Flags waren irgendwo unterwegs verlorengegangen, und das Resultat kein bißchen brauchbarer als beim ersten Versuch.

    Dabei bin ich eigentlich froh und dankbar, daß der gcc als Buildsystem die GNU Autotools verwendet. Sie werden zwar manchmal als veraltet und zu kompliziert abgetan, aber ich komme mit ihnen immer noch weit besser klar als mit CMake, Python Distutils und allem anderen, das ich bislang gesehen habe. Die Probleme beim gcc rühren allein daher, daß es mit dem bloßen Kompilieren nicht getan ist; stattdessen wird der dabei erzeugte Compiler dazu verwendet, aus dem Sourcecode noch einen Compiler (Stage2) zu erzeugen, und dieser wiederum erzeugt dann das fertige Kompilat (Stage3). ((Dieser Bootstrap genannte Zauber dient dazu, den fertigen Compiler mit sich selbst zu kompilieren, was ein guter Test für seine Zuverlässigkeit ist. )) Of will man in verschiedenen Stadien verschiedene Optionen verwenden, und deshalb gibt es auch einen ganzen Zoo von Umgebungsvariablen, deren Zweck nicht immer ohne weiteres klar ist.

    Ach so, die Lösung: nach dem Konfigurieren einfach make BOOT_CFLAGS='-g -O0' bootstrap eingeben, und schon klappt es.

  • Bootstrap

    Eine kurze Statusmeldung: Inzwischen läuft der Build durch, und ein passendes Problemchen zur Analyse habe ich auch schon gefunden. Am Anfang ist es immer ratsam, sich einen weniger drängenden Bug zu suchen, weil es sonst leicht passiert, daß jemand mit mehr Erfahrung und Überblick schneller ist…

  • Dreaming of Code

    Es war vor ein paar Tagen, da saß ich in meinem Lieblingssessel, es war etwas früher als üblich, und es sollte ein schöner Abend werden. Endlich die Gelegenheit, etwas zu tun, zu dem mir sonst die Zeit fehlt — doch was nur? Lesen mochte ich aus irgendeinem Grund nicht, und der Vokabelkasten neben mir wirkte auch nicht gerade verlockend. Ein Computerspiel vielleicht, dachte ich mir, wenn die Monster zur Tür hereinkommen und du die Taschenlampen und Bumerangs strategisch ums Bett herum verteilst ist das sehr befriedigend, weil die Kiste dir mit jeder Monsterwelle eine neue Herausforderung vorwirft aber du löst sie jedesmal und die Lösung ist so einfach und so elegant wenn du nur die Taschenlampen hinten in die Kurven und die Shuriken vorne an die Geraden stellst, aber nein irgendwie ist das ja auch alles repetitiv und ein bißchen langeweilig, und dann wußte ich du brauchst Code code CODE und es ist völlig egal daß du jeden Tag acht Stunden am Rechner verbringst du mußt jetzt und gerade den Compiler anwerfen und ein programmieren und jedes Problem ist eine Herausforderung aber das Programm löst sie und der Code ist so elegant nur ist es gar nicht repetitiv wenn du nur das richtige Problem hast und hinterher können tatsächlich Leute dein Programm benutzen und…

    Nun ja, ich habe dann ein bißchen nach einem passenden Projekt gesucht. Vielleicht ein schönes buntes Mac-Programm? Aber bald fiel mir wieder ein, daß ich vor fünf oder sechs Jahren schonmal ein bißchen im gcc herumgefuhrwerkt hatte, und das hat mir eigentlich von allen Projekten immer noch am meisten Spaß gemacht: einerseits ist der Compilerbau schon soetwas wie die Königsdisziplin der angewandten Informatik, und andererseits gibt es beim gcc unglaublich viele kleine Nischen und Unterprojekte, in denen man sich nicht gegenseitig auf die Füße tritt, man aber auch Chancen hat, daß der eigene Code hinterher im fertigen Produkt Verwendung findet. Naja, und dann hat der gcc natürlich eine sehr zentrale Rolle im GNU-Projekt und eine unglaublich breite Nutzerschaft, und das schmeichelt dem Ego dann auch irgendwie.

    Für’s erste ist aber statt Blood, Sweat & Code noch der Kampf mit dem Buildsystem angesagt, damit ich den ersten Bootstrap hinbekomme.

  • End Of File

    [lang_de]Heute habe ich mal wieder eine Notiz, die für die meisten Leser wohl weniger interessant sein dürfte.

    Wer Jim Rogers‘ Pipe Commands für Ada verwendet und über den Linkerfehler
    undefined reference to `c_constant_eof'
    stolpert, der möge es einmal mit
    pragma Import (C, c_constant_EOF, "__gnat_constant_eof");
    anstelle von
    pragma Import (C, c_constant_EOF);
    probieren.[/lang_de]

    [lang_en]This is again an entry bound to be uninteresting to most…

    If you use Jim Rogers‘ Pipe Commands for Ada, and the linker complains about an
    undefined reference to `c_constant_eof',
    try
    pragma Import (C, c_constant_EOF, "__gnat_constant_eof");
    instead of
    pragma Import (C, c_constant_EOF);
    [/lang_en]

    [via Usenet]

  • A, B, C, C++

    Es war einmal eine Zeit, in der für jeden neuen Computer alle Programme neu geschrieben werden mußten. Die Menschen kannten es nicht anders, und so erfanden sie tagein, tagaus das Rad neu. Doch dann kam Dennis und sagte: wäre es nicht schön, wenn wir dem Computer einfach erklären könnten, was die Programme tun sollen? Dann könnte der Computer das Programm selber schreiben; und wenn wir einen neuen bauen, dann geben wir ihm einfach die gleiche Erklärung, und er baut sich das Programm so, wie er mag.

    So hat Dennis die Programmiersprache C erfunden. Außerdem hat er noch einen guten Teil von Unix erfunden, aber das ist eine andere Geschichte. Ein paar Jahre später hat Bjarne C++ erfunden. C++ ist ein bißchen seltsam: einerseits ist es ein einfaches Werkzeug für Leute, die sich beim Arbeiten die Hände dreckig machen (low level, sagt der Programmierer), wie C es ist: so etwas wie ein Hammer oder eine Zange; andererseits bringt es eine Menge fortschrittliches Zeugs mit: wie ein Industrieroboter vielleicht.

    Kein Wunder, daß es da Ungereimtheiten gibt. Wer sich mit C++ auskennt, der findet bei yosefk eine sehr unterhaltsame Zusammenstellung dieser Ungereimtheiten.

    [Edit: Typo]

  • Schwierigkeiten

    Software is hard

    hat Donald Knuth, graue Eminenz der Informatik, einmal gesagt. Warum das so ist, versucht Scott Rosenberg in seinem Buch Dreaming In Code zu ergründen.
    Er tut das in einer Form, die mich sehr an ein Blog erinnert: die Kapitel bestehen nicht aus einem durchgehenden Erzählstrang, sondern aus oft nur lose zusammenhängenden, kurzen Abschnitten; dabei springt Rosenberg oft zwischen den Anfängen der Computertechnik und der Gegenwart hin und her, und man merkt, daß Hoffnungen und Probleme sich doch über die Zeiten kaum verändert haben.

    … Bugs are called „defects,“ and defects are „injected“ by workers–as if the product begins in some Platonic state of perfection and is then corrupted by mad-eyed workers shooting bug-filled syringes into its bloodstream.�

    Ein weiteres Merkmal von Blogs ist das Verlinken auf Quellen oder verwandte Themen. Hyperlinks funktionieren in einem Buch natürlich nicht, aber dafür gibt es fast dreißig Seiten Fußnoten mit Referenzen, viele sogar mit URL.

    Eine eindeutige Antwort kann der Autor letztlich nicht liefern, aber er zeigt doch eine Menge Aspekte auf, die Softwareprojekten zusetzen. Der für mich wichtigste Punkt betrifft die Frage, warum Brückenbauten in der Regel problemlos über die Bühne gehen, das Erstellen von Programmen aber nicht:

    Software development is often compared to the construction industry, but the analogy breaks down in one respect. Even after we have learned how to build structures so solve particular problems … we still need to keep building more of those structures. However much I may like your house, I can’t have it myself.�

    Abschließend möchte ich noch hinzufügen, daß Rosenberg ausdrücklich Nichtprogrammierer als Zielgruppe anspricht. Er verzichtet weitgehend auf technische Details, und erklärt diese, wenn er sie trotzdem anspricht. Gerade diesen Lesern bietet Dreaming In Code die Möglichkeit, zu erfahren, wie Softwareentwicklung funktioniert — welche Probleme sich auftun, wie die Entwickler zusammenarbeiten, was sie motiviert.

    Politischer Aktivismus ist übrigens auch schwierig. Wolfgang Stieler beschreibt das recht witzig (natürlich aus der Sicht eines Softwareentwicklers), aber das Thema und sein Fazit sind durchaus ernst:

    Die meisten politischen Angelegenheiten werden außerhalb des Netzes verhandelt.

    Da nimmt es nicht wunder, wenn auch monatelanger Aktivismus (natürlich zum großen Teil online quer durch die Blogosphäre) in der Bundespolitik kaum Wirkung entfaltet.