Warum machen Erdlinge fehlerhafte Software und Hardware?

    Ich denke, niemand wird mit der Tatsache argumentieren, dass die Qualität der komplexen Systeme, die von den Erdlingen geschaffen werden, alles andere als ideal ist. Man kann natürlich sagen, dass alles funktioniert - Flugzeuge fliegen, Raumschiffe fahren durch die Umlaufbahnen der Erde usw.

    Gleichzeitig gewöhnte sich jeder daran, dass die Software auf ihren Geräten einmal unvorhersehbar funktioniert, und dass selbst das Installieren der neuesten Updates nicht das Fehlen von Sicherheitsproblemen garantiert, die häufig in offenem, massiv verwendetem Code Fehler finden, die dort jahrelang bestehen, die sogar bestehen Große und "technologische" Unternehmen sind Ausfälle und Datenlecks, die dazu führen, dass Raumfahrzeuge kaputt gehen oder einen Teil der Funktionalität verlieren, nicht aufgrund der Intrigen von Außerirdischen (die Marsianer schwören, dass sie keine ExoMars erschossen haben).

    Ich möchte die Ursachen und möglichen Lösungen für dieses Planetenproblem prüfen.

    1. Der Mangel an Professionalität und Inkompetenz der Darsteller - Erdlinge werden meistens nicht gelehrt und sind nicht daran gewöhnt, ihre Arbeit gut zu machen. Dieses Problem ist sehr ernst, und Sie können lange darüber reden, aber anscheinend müssen Sie einen separaten Beitrag schreiben. Hier kann man nur sagen, dass es echte Profis gibt, es sollte genug für fortgeschrittene Projekte sein, aber es gibt Probleme bei solchen Projekten, daher ist dies nicht die einzige Sache.

    2. Fehlende Ziele / schlechtes Management / unzureichende Investitionen - dies ist bei gewöhnlichen kommerziellen Projekten sehr wahrscheinlich, bei denen die Aufgabe darin besteht, kurzfristigen Gewinn zu erzielen und nicht gut abzuschneiden. Dabei handelt es sich eindeutig nicht um Weltraumprojekte, bei denen die Kosten eines Fehlers in Bezug auf Geld und Reputation zu hoch sind und die Entwicklungskosten nach einigen Schätzungen 160-mal höher sind als die übliche kommerzielle Entwicklung, aber auch ohne Zuverlässigkeitsgarantie.

    3. Mit ungeeigneten Werkzeugen / Versuchen, eine Linse mit einem Hammer zu schleifen - dies scheint mir der Hauptgrund zu sein, und ich werde später darüber sprechen. Ehrliche Programmierer sagen wegen des falschen Lösungsansatzes niemals "Ja, es funktioniert", aber sie sagen: "Es scheint zu funktionieren", "Muss funktionieren".

    Wenn sich die Erdlinge mit den schwierigsten Aufgaben befassen, die sich ihnen stellen, ist es logisch, die besten verfügbaren Werkzeuge einzusetzen, um sie zu lösen.
    Und dieses Werkzeug ist definitiv kein menschliches Gehirn , das Gehirn des Homo sapiens ist nur ein Werkzeug aus der Reihe "scheint zu funktionieren", und Sie sollten nicht überrascht sein, es hat sich für ganz andere Aufgaben entwickelt, so dass selbst der coolste Profi einen langweiligen Fehler auf dem Haufen machen kann Gründe.

    Wenn Sie viele gute Gehirne zusammenbringen, können Sie natürlich das Ergebnis verbessern, aber ohne ein gutes Werkzeug werden alle Gehirne des Planeten nicht das erreichen, was bereits erreicht wurde.

    Um zu verstehen, was für ein magisches Werkzeug es ist, sollten Sie versuchen, die folgenden Fragen zu beantworten: "Warum kollabieren Wolkenkratzer nicht unter ihrem Gewicht oder im Wind?", "Wie kommt unser Raumschiff in den riesigen Weiten des Weltraums zum Ziel?", "Wie schaffen wir es, Daten zuverlässig zu senden über unzuverlässige Kommunikationskanäle? "," Woher stammen zuverlässige Verschlüsselungsmethoden? "und so weiter und so fort.

    Die Antwort auf alle diese Fragen ist eine, dieses Werkzeug ist Mathematik . Mathematik ist der Zauber der modernen Welt, für Uneingeweihte Artefakte wie Zcash oder CryptDB , und wie üblich sieht die asymmetrische Verschlüsselung aus wie Magie, obwohl dies nur die Verwendung dieses mächtigen Werkzeugs ist.

    Um zu sagen: "Ja, das Programm funktioniert wie gefordert", muss man einen mathematischen Beweis für diese Aussage haben. Leider bin ich kein Experte auf diesem Gebiet, aber soweit ich weiß, ist der Ablauf dieses Nachweises ziemlich kompliziert, aber dies sollte aus folgenden Gründen kein Hindernis sein:

    1. Es gibt keinen anderen Weg, unsere Systeme werden komplexer, die neuen Schichten basieren auf den alten, aber leider ist dies kein sehr zuverlässiges Fundament.

    2. Sie müssen kleine Programme nachweisen ( Unix-Weg ).

    3. Es muss lediglich der Nachweis erbracht werden, dass die Programme sicherheitskritisch sind. Sie können die Korrektheit der Office-Suite nicht nachweisen, der Betriebssystem-Mikrokernel oder die Verschlüsselungsbibliotheken müssen jedoch nachgewiesen werden.

    4. Beweisen Sie nicht notwendigerweise eine vorhandene Universalsoftware, nicht notwendigerweise ein allgemeines Betriebssystem, vielleicht etwas Einfacheres, ohne Pfeifen, aber so zuverlässig wie möglich für Medizin, Verkehr und Kernkraftwerke.

    5. Die Verwendung streng mathematischer Programmiersprachen kann die Beweiskosten reduzieren ( Haskell ?). Ja, sie können etwas komplizierter sein als gewöhnliche PLs, aber ihre Komplexität entspricht der Komplexität der Aufgaben, die angesprochen werden müssen.

    6. Es ist nicht notwendig, alles auf einmal zu beweisen, aber Sie können schrittweise eine bewährte Infrastruktur für den Aufbau zuverlässiger Systeme aufbauen.

    Natürlich behebt der Programmnachweis nicht die Notwendigkeit, Anforderungen präzise zu formulieren, aber ich denke, dass dies eine lösbare Aufgabe ist, zumal in einigen Fällen (wie Verschlüsselungsbibliotheken) auch die Anforderungen selbst formalisiert werden.

    Ich denke, jeder möchte absolut zuverlässige Software, die in Kernkraftwerken, in medizinischen Geräten und an ähnlichen Orten zum Einsatz kommt.

    Ich werde nicht behaupten, dass dies vor langer Zeit notwendig war, die Branche boomte, viele Dinge haben sich erheblich verändert, aber heute ist die Branche aus meiner Sicht reif genug, um die Dinge in Ordnung zu bringen.

    Es gibt neue Aufgabenklassen wie Quantencomputer und spezialisierte Prozessoren für neuronale Netze. Hier fängt alles erst an. Die Entwicklung dieser Industrien macht jedoch die Notwendigkeit des klassischen Ansatzes nicht zunichte - alle haben ihre eigenen Aufgaben.

    Die Zivilisation der Erde ist bereits sehr abhängig von der Zuverlässigkeit von Computersystemen. Um nachts vor dem Flügelgeräusch eines fliegenden Spechts nicht zu schrecken, muss nach Lösungen gesucht werden, die die Zuverlässigkeit erhöhen.

    Specht? Und hier der Specht
    Dies ist ein altes Mem: "Wenn Bauarbeiter Häuser bauten, als Programmierer Programme schreiben, dann würde der erste Vagabundspecht die Zivilisation zerstören"

    Unabhängig davon ist über neuronale Netze zu sagen. Neuronale Netzwerke sind ein Versuch, das Gehirn mit all seinen Vor-und Nachteilen zu replizieren. Die Lösung in neuronalen Netzwerken enthält dieselben Probleme wie das menschliche Gehirn. Daher sollten sie nur verwendet werden, wenn wir nicht wissen, wie sie das Problem mithilfe von formalen Problemen lösen können Der Algorithmus arbeitet absolut zuverlässig.

    Ich denke, für eine stetige Entwicklung der Zivilisation der Erde ist es an der Zeit, über die Zuverlässigkeit ihrer Infrastruktur nachzudenken. In Bezug auf die IT scheint es mir so: Sie müssen eine hochrangige mathematische Programmiersprache auswählen und erstellen und sie vollständig (ohne versteckte sichnyh lib) unter der Haube erstellen ihre nachfolgenden Beweise. Es ist wahrscheinlich, dass die Hardware-Architektur der Prozessoren für die Ausführung von Programmen in einer solchen Sprache nachgewiesen und geschärft werden muss (lisp-maschine ?).

    Wer soll das machen? Ich weiß es nicht, aber die gleiche Frage hätte auch gestellt werden können, um den Kernel des Betriebssystems für die ganze Welt zu schreiben, aber Linux ist vollständig geschrieben, was bedeutet, dass es Optionen gibt. Zum Beispiel gibt es einen formal verifizierten seL4- Kern ( erklärt in seinem Wiki ), der von NICTA entwickelt wurde. Wenn solche Projekte nicht zur Grundlage für die digitale Infrastruktur der Zukunft werden, wird die Menschheit die Chance haben, den großen Filter der Zivilisationen nicht durchzugehen (wer ist sicher, dass das Virus keinen Atomkrieg auslösen wird).
    einige texte
    Планету больше не закрывали белые стаи облаков, с ее лица сползли остатки зелени и голубизны. По поверхности пробегали, искрясь и подмигивая звездами в вышине, сверкающие цепочки огней, и оттуда, как в танце сказочных фей, поднимали к небу свои лепестки, переливающиеся всеми оттенками нежнейше черного цвета, благоухающим ароматом ультракороткого излучения, пышные, пенящиеся и мерцающие своей хрупкой, утонченной красотой атомные орхидеи.

    — Это чудо… чудо! О, как великолепно!

    — Да. Это самое прекрасное из того, что я только видел во Вселенной…

    — Наверное, планеты и существуют для того, чтобы распуститься только один раз… Но разве этого мало?..

    «Когда расцветают бомбы» Роджер Желязны Сергей Битюцкий

    AKTUALISIERUNG: Während der Diskussion in den Kommentaren ist eine wichtige Idee herangereift: Um verifizierte Software in kritischen Bereichen zu implementieren, ist es nicht notwendig, die aktuelle Entwicklung zu stoppen, Sie müssen gleichzeitig kostenlose verifizierte Komponenten erstellen und für ihre Bereitschaft, mit ihrer Hilfe Neues zu tun, beispielsweise den oben genannten seL4-Mikrokernel für Embedded-Anforderungen bereits, also müssen Sie es verwenden, wo immer es passt. Und an anderen Komponenten arbeiten.

    Jetzt auch beliebt: