Avatar von Gernotius
  • Gernotius

762 Beiträge seit 26.01.2021

Der Coder läuft mit dem Kopf so lange gegen die Wand, bis er die Tür findet?

Was hier im Artikel beschrieben ist, hat mit solider Ingenieursarbeit nichts zu tun. Das ist mehr "Try and Error!".

Sichere, fehlerfreie Software wird z.B. zuerst in F* formuliert. Dann läßt man daß über einen Solver (z.B. Z3) laufen, der sämtliche Kombinationen von 'state', die ein Programm einnehmen kann, systematisch absucht. Und wenn da keine Endlosschleifen im Graphen sind ("Programm hängt!") und keine undefinierten Referenzen, Abzweigungen nach Nirgendwo ("Bluescreen"), dann kann das zumindest als "fehlerfrei" und "stabil" klassifiziert werden. Ob es das tut, was es soll, klärt man dann über Unittests ab.

Hier ein Beispiel, wie das in der Praxis funktioniert:

https://arxiv.org/pdf/1803.06547

Weitere Info's hier:

https://project-everest.github.io/

Und eine sehr lehrreiche Video Serie mit dem Turing Preisträger Leslie Lamport, der auch CosmosDB mit designt hat:

TLA+ Video Course: https://youtube.com/channel/UCajiu4Cj_GHOX0if3Up-eRA

Darunter würde ich mich nicht einmal als "Programmierer" geschweige denn als "Software Ingenieur" bezeichnen. Was dabei heraus kommt, sieht man ja hier, the "never ending story":

https://www.heise.de/news/Jetzt-patchen-Angreifer-attackieren-Microsoft-Exchange-Server-5070309.html

Bewerten
- +