Logic for Programmers: Wie Mathematik Software besser macht
Ich habe ein Buch geschrieben, das zeigt, wie Logik das Design und die Verifikation von Software verbessert. Ohne tiefes Mathematikwissen erlernen erfahrene Entwickler praktische Techniken, von der Vereinfachung von Bedingungen bis zur formellen Verifikation mit Dafny. Jeder Kapitel ist unabhängig und bietet konkrete Anwendungen für den Alltag.
In Python ist all([]) == True, weil True die Identität des Und-Operators ist und diese Eigenschaft für jede Liste erhalten bleiben muss.
- rmunn
Als ich noch Student war, habe ich aus Spaß einige Philosophievorlesungen belegt. Als ich dann Symbolische Logik nahm, stellte ich fest, dass ich die Vorlesung ziemlich leicht fand, während alle anderen damit kämpften, denn das Verketten eines Beweises in der symbolischen Logik fühlte sich genau wie Programmieren an. Es waren die gleichen mentalen Schritte: Man hat die Ausgangsbedingungen, es gibt ein Ziel, das man erreichen möchte, und man muss diese grundlegenden Operationen verketten, um dorthin zu gelangen. (Und manchmal musste man sehen, wie man sie aufbrechen kann: Wenn man P UND Q beweisen muss, waren das separate Beweisen von P und das separate Beweisen von Q meist einfachere Schritte, und sobald man P und Q bewiesen hat, hat man auch P UND Q bewiesen. Das fühlte sich sehr ähnlich an wie das Refactoring einer großen Funktion, die zwei Dinge macht, in zwei separate, kleinere Funktionen, die jeweils nur eine Sache tun).
Wenn ich mir das Beispielkapitel anschaue, erinnert es mich an meine Erfahrung mit der Vorlesung zur symbolischen Logik. Es sieht so aus, als wäre es im Grunde dasselbe, nur auf den Kopf gestellt: Statt Programmieren zu kennen und dieses Wissen zu nutzen, um symbolische Logik einfacher zu machen, geht es hier wohl darum, symbolische Logik zu kennen und dieses Wissen zu nutzen, um Programmieren einfacher zu machen. Klingt ziemlich nützlich; ich werde mir die Beispielkapitel bald genauer ansehen.
- js8
Sieht aus wie ein schönes Buch, aber... Ich habe das Gefühl, dass keine ernsthafte Arbeit mit diesem Anspruch heute die Curry-Howard-Isomorphie, Propositions-as-Types und die daraus folgende Analogie zwischen Logik und Lambda-Kalkül auslassen sollte (vielleicht ist es ja enthalten, bin mir vom Inhaltsverzeichnis her nicht sicher).
Das hier gefällt mir wirklich: https://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard....
Ich denke, jeder Programmierer sollte die Konsequenzen der CHI für die Disziplin verstehen, die tiefgreifend sind. Es bedeutet, dass es keinen Bedarf an klassischer Logik als separate Metasprache gibt; die Eigenschaften von Programmen könnten auch in der Programmiersprache Ihrer Wahl ausgedrückt werden. Darüber hinaus zeigt es, dass "das Programm ausführen" und "über das Programm nachdenken" letztlich dieselben Prozesse sind, was einige gute philosophische Fragen aufwirft, etwa zum Thema Testing. Aber auch darüber, wie wir den Programmentwurf angehen können; vielleicht können wir ihn einfach aus den Constraints "berechnen". Es öffnet uns auch Dinge wie Superkompilierung.
Ich denke, die Disziplin muss sich in Richtung eines formalen Verständnisses bewegen, wie verschiedene Programmiersprachen und Logiken ähnliche Ideen ausdrücken, denn das ist ein wirklich mächtiges Werkzeug des gegenseitigen Verständnisses.
(Außerdem finde ich persönlich die typisierte LC-Notation, besonders mit Typüberprüfung und Typinferenz, einfacher als die klassische Logik-Notation. Das könnte der Grund sein, warum Logik als zu kompliziert gilt.)
- mirrorlake
Ich freue mich darauf, das zu lesen; ich bin einer derjenigen, die es vorbestellt haben. Ich habe oft gehört, dass Menschen mit Abschlüssen bereuen, in diesem Buchmaterial nicht besser gewesen zu sein, also wird dies für viele Menschen eine Chance sein, diese Fähigkeiten auf eine Weise zu üben, die ihre Abschlüsse in Informatik/Mathematik/Physik/Ingenieurwesen ihnen nicht wirklich ermöglichten.
Außerdem hat Hillel (der Autor) einen Blog, der sich absolut lohnt, und einige großartige Vorträge auf Konferenzen, die auf YouTube zu finden sind. Er gehört zu den wenigen Rednern, deren Vorträge ich automatisch anschaue.
- Merkur
Ich habe den kostenlosen Teil gelesen. Sieht interessant aus, aber das mathematische Erbe dominiert, wie versprochen.
Es scheint den kompakten und effizienten Code-Typ zu bevorzugen, der in den Händen eines mittelmäßig kompetenten Junior-Entwicklers oder eines stark multitaskingenden Senior-Entwicklers spröde ist.
Ich mag klugen Code in lustigen Projekten, aber bei der Arbeit bevorzuge ich Code, der schnell zu lesen und zu verstehen ist. Versuchen Sie nicht, fancy zu sein.
Also nehme ich an, dass dies ein Buch ist, das meine Annahmen herausfordert. Das mag ich. Danke.
- mjaniczek
Herzlichen Glückwunsch an Hillel, dass er das Buch fertiggestellt hat!