Sowas ist nett. Gute Software ist eine Ächtung aller miesen Lame-Progger.
Interessant wenn man sieht, das samba,tor,ruby auf der Super-Liste überguter Software stehen.
Beweisbarkeit wird kommen.
Die Methoden sind i.d.R. eine Bildschirmseite. Die Rechenleistung ist seit früher massiv vermehrt (verdoppelt alle 15-18 Monate) so das Beweise möglich sind.
Weiteres in meinen anderen Postings zu beweisbarkeit.
Nur weil Leute theorien gödel falsch verstehen, diskutier ich hier nicht mit denen.
Es geht nicht darum, jedes Programm zu checken.
Das Eich-Amt misst/eicht ja auch nur gewerbliche Waagen.
Ein Projekt möchte gern bewiesen sein, dann kann es den code auch beweiser-freundlicher schreiben.
Es geht nicht darum, jeden zufällig zusammengewürfelten C-Code der compilierbar ist, zu beweisen.
Und Korrektheit ist nur ein Peanut. Zahl der Plattenzugriffe, bandbreite auf begrenzter Bus-Bandbreite usw. sind genau so wichtige Metriken die man ggf. beweisen möchte.
Und wo ordnen wir dabei Firefox ein? Ist ja auch Open Source. Gleichzeitig aber vollkommen unbrauchbar und vermutlich was den Code angeht total vergurkt.
Deswegen nehme ich normalerweise Opera.
google-Reader geht in Firefox viel besser und Amazon hat EINEN Link beim Marketplace reinstellen wo man leider auch firefox nehmen muss.
Ich habe auch nirgendwo behauptet, das Open Source besser wäre.
Hier gehts um Beweisbarkeit und nicht um Open Source.
Allerdings könnten natürlich geschulte sweeper-teams beweiser-hints bzw. conditions/vor-nachbedingungen an kernel-module dranhängen. oder halt "anti-beweise" wo klar wird, das spacko-treiber-progger mal wieder scheisse gebaut hat.
beides macht sinn (fehler finden, beweise bauen).
Seit wann ist der unbrauchbar?
Ein Tool kann niemals die Richtigkeit oder Korrektheit eines anderen Tools beweisen. Denn dazu müste es erst einmal sich selber die Richtigkeit oder Korrektheit beweisen. Das geht aber nicht ;)
Daher sind solche Tools zwar Praktisch aber niemals ein Ersatz für ausführliche Beta Tests.
Häh ?
Ein Beweis ist eine endliche Ableitungskette.
Das Tool kann so kommunistisch, cdu-freundlich, gehirnamputiert, likes, rechts, oben unten, falsch-rum sein wie es will.
Wenn es eine endliche !KORREKTE! Ableitungs-Kette erzeugt, die den Beweis erbringt, ist egal, wie herum das Tool ist.
Das ist der "Trick" dabei. Einen !maschinellen! Beweis (bzw. Ableitungs-Kette) kann man IMMER Überprüfen. So wie man beispielsweise die linke und rechte Seite einer Bilanz zusammenzählen kann und gucken kann, ob beide Seiten exakt denselben Wert liefern (was sie müssen).
Es gibt Beweise, die man lange für welche hielt, aber doch keine waren. Aber das waren halt keine maschinell überprüfbaren Ableitungsketten.
Das ist dann eher so wie wenn man im Multiple Choice was ankreuzt was richtig oder falsch ist, aber seine Rechnung nicht auf dem Prüfungsblatt (oder Bei-Blatt) ablegen muss. Was man für Kopfrechnung nicht muss, aber bei richtigeren Prüfungen höherer "DAN"-Level/Schulstufen/UNI schon.
Bei maschinellen Beweisen ist die Überprüfung geilerweise aber möglich.
So wie gute Zitate/Plagiatismus auch einfach erkennbar ist. Bei den guten Zitaten ist eine [Hanswurst 1998]-Quellen-Angabe. Böse Zitate sind dasselber aber ohne Quellenangabe. Das ist so ähnlich wie "selbstjustierend", weil man Plagiatismus-Checker-Tools auch mit guten/korrekten Texten checkern kann.
Du hast aber indirekt Recht, das ein fehlerhaftes Tool i.d.R. fehlerhafte also ungültige Beweise abliefern wird.
So wie Bundeswehrsoldaten die zickzacklinien bei Umfragen/IQ-Tests ankreuzen, zu denen sie "zwangsrekrutiert" oder mit einer Flasche Bier/Packung Schokolade/Zigaretten geködert wurden.
Siga9876 schrieb:
--------------------------------------------------------------------------------
> Beweisbarkeit wird kommen.
Nein. Nur die Beweisbarkeit, dass die Implementierung des Spezifikation entspricht, aber wie willst Du beweisen, dass die Spezifikation korrekt ist? Du kannst das Beweisproblem immer weiter nach Vorne verlagern, aber wenn Du beim Menschen angekommen bist, geht es nicht weiter. Somit sind autom. Beweissysteme IMHO relativ sinnlos.
Arti
Spezifikation schreiben ist also sinnlos. Na super Einstellung.
Man beweist nicht nur die Spezifikation.
Man beweist viel geilere Sachen: Das diese Implementierung mit einer bestimmten Bandbreite auskommt. ODer bestimmte Latenz-Anforderungen erfüllt. oder pro Client maximal x Blöcke von der Platte braucht weshalb man garantieren kann, das der durchsatz für x,000 Flugzeuge und FlugZeug-Routen-Lotsen-Software reicht.
Amis haben fette vermutlich überlastete Infrastrukturen die noch nicht ansatzweise zusammengebrochen sind. Dafür brauchts nichtmal terroristen. der fette stromausfall vor ein paar Jahren der ganze bundesländer/us-staaten oder dieses Jahr Hamburg stromfrei legte, beweisen es.
Na gut. Egal. Beweisen muss so laufen wie bart simpson der mit irgendjemand anderem im wettbewerb steht und "ich kann auch bungejumpen" "Ich kann über den fluss springen" "Ich kann über die stromleitung spazieren" "ich kann mit dem skateboard über die chemikalen-tanks skatern"... ständig eskaliert.
Wenn man mal Modelle für attacken hat (was nicht notwendig bedeutet das andere attacken nicht gehen), kann man alle software unterziehen. und im öffentlichen/sicherheitskritischen(flugzeuge, krankenhaus,...) bereich sollte man es einfach machen.
Du hast aber vollkommen Recht, das die Spezifikation ein Risikofaktor ist.
Aber zu beweisen, das keine buffer-overflows, keine lecks,... (bekannter Sorte) vorhanden sind, ist auch schon mal etwas.
> Du kannst das Beweisproblem immer weiter nach Vorne verlagern
Ja, bis zur Ursuppe. Deshalb gibt es leckere Sachen wie Axiome, Methodik und anderes wissenschafftliches Vodoo. Man munkelt gar, selbst angewandte Mathematik funktioniere ohne pseudointellektuelles Zerreden.
Spacken haben Angst vor Neuem, weil es ihre evolutionsmößig hinterwäldlerische Existenz bedroht.
Das ist kein Zerrede. Da gehts darum, absichtlich minderwertig zu proggern.
Immer weiter verlagern geht auch nicht. Da hat er vermutlich Unrecht. ABer er hat Recht, das man sehr genau wissen muss, was man beweisen will.
Boyer-Moore-Buch über ihren Beweiser (für eine !eingeschränkte! Logik) gabs das Beispiel von Sortieralgorithmen: Da hat der Beweiser bewiesen, das der Sortieralgorithmus korrekt ist. Doof nur das der Algorithmus nur die leere Liste lieferte. Da hat man in der Spezifikation vergessen, reinzuschraiben, das die Elemente nicht nur sortiert sein müssen (das hatte man nicht vergessen), sondern auch alle Elemente die vorher drin ware, auch nach dem Sortieren drin sein müssen.
Die einfachste sortierte Liste ist halt die leere Liste.
Von daher ist das Argument mit der schlechten Spezifikation schon korrekt.
Bei Optimierung sieht man schnell, das man z.b. x1>=0 vergessen hat, wenn plötzlich negative Werte rumkommen z.b. für Umsatz-Optimale Müsli-Mischungen. Aber in Realität dürften viele Optimierungssysteme mit leicht falschen Parametern gefüttert sein so das nicht wirklich die optimale Lösung ausgespuckt wird. Fällt halt bei 20 oder mehr Variablen nicht weiter auf.
Man müsste immer doppelt und dreifach drübergucken.
Und bei Standard-Libs sollte es NULL/KEINE Buffer-Overflows, NULLpointer-Fehler usw. mehr geben. Sowas sollte Steinzeit sein.
Und das etwas die Specs erfüllt, heisst nicht, das es bei fehlerhaften Daten keine Buffer-Overflows hat. Aber genau geht es ja auch: AUCH den Schutz vor Buffer-overflows bei bösen Daten.
> Denn dazu müste es erst einmal sich selber die Richtigkeit oder Korrektheit beweisen.
Blödsinn, das kann ein Mensch machen.
> Ein Tool kann niemals die Richtigkeit oder Korrektheit eines anderen Tools beweisen. Denn dazu müste es erst einmal sich selber die Richtigkeit oder Korrektheit beweisen. Das geht aber nicht ;)
Kommt auf die Komplexität des Tools an. ^^
___
Die ganz grossen Wahrheiten sind EINFACH!
Wirkung und Gegenwirkung.
Variation und Selektion.
Wie im grossen, so im kleinen.
> bei Standard-Libs sollte es NULL/KEINE Buffer-Overflows, NULLpointer-Fehler usw. mehr geben. Sowas sollte Steinzeit sein.
Mich wundert das der Compiler nicht die Programme auf sowas checkt!
___
Die ganz grossen Wahrheiten sind EINFACH!
Wirkung und Gegenwirkung.
Variation und Selektion.
Wie im grossen, so im kleinen.
Der Kaiser! schrieb:
--------------------------------------------------------------------------------
> > bei Standard-Libs sollte es NULL/KEINE Buffer-Overflows,
> NULLpointer-Fehler usw. mehr geben. Sowas sollte Steinzeit sein.
> Mich wundert das der Compiler nicht die Programme auf sowas checkt!
In moderneren Sprachen gibts im Speicher herumpoken ja nicht mehr. Danke.
Wenn man gcc -Wall (iirc) einschaltet, kriegt man auch bessere Fehlermeldungen.
Früher gabs separat z.b. "lint" dafür. Weil die Kisten lahm waren und man zillionen Zeilen übersetzen musste ("make world" bei ***BSD als Beispiel) hat man Code-Checking und einfach nur schnell mal compilieren getrennt gehalten. Dann hat man code-checking einfach sein lassen... Spacken-progger-Pack.
Momentan ist es leider immer noch eine Einstellung anständig programmieren zu wollen. Spacken-Progger-Packs sollte aber nix anderes übrig bleiben.
Davon abgesehen sollte man mehr configuren (rollen/Datenbasiert) und automatisiert 90% des codes erzeugen und nur echte Aufgaben wirklich seölber proggern. aber in vielen business-bereichen ist es eh nur daten verschieben und z.b. in der warenwirtschaft die bestellten produkte im bestand herunterzählen. oder kfz-nummern mit versicherungsnummern und adresse des auto-eigentümers verbinden. Das macht die primitive datenbank.
das konfiguriert man einmal und ein billiger ScreenDesigner macht die CSS für die Daten für die Bürger-interfaces und beamten-interfaces. aber so weit ist proggertum leider noch nicht.
im praktikum habe ich sowas wie javadoc "erfunden" und mir aus kommentaren die doku in latex automatisiert zusammengestellt.
sowas wie hibernate (natürlich primitiver) hätte ich mir auch erfunden, wenns das nicht schon gäbe.
jetzt fehlt noch rollen+daten und primitiv-software wird/bleibt primitiv. und alle haben einen nutzen.
>>> bei Standard-Libs sollte es NULL/KEINE Buffer-Overflows, NULLpointer-Fehler usw. mehr geben. Sowas sollte Steinzeit sein.
>> Mich wundert das der Compiler nicht die Programme auf sowas checkt!
> In moderneren Sprachen gibts im Speicher herumpoken ja nicht mehr. Danke.
Man sollte aber bei Bedarf das trotzdem machen können.
___
Die ganz grossen Wahrheiten sind EINFACH!
Wirkung und Gegenwirkung.
Variation und Selektion.
Wie im grossen, so im kleinen.
Kommentare: 222 | letzter Beitrag 26.05. 23:51
Kommentare: 216 | letzter Beitrag 00:27 Uhr
Kommentare: 161 | letzter Beitrag 09:43 Uhr
Kommentare: 93 | letzter Beitrag 26.05. 19:45
Kommentare: 66 | letzter Beitrag 08:55 Uhr
E-Mail an news@golem.de
Ein soziales Netzwerk für Pornografie muss seine Marke nicht an Facebook übergeben. Faceporn, ein norwegisches Unternehmen, freut sich über den Sieg vor einem kalifornischen Gericht.
Diablo 3 ist toll, sagen viele Spieler - Diablo 3 ist eine Stimulus-Response-Maschine, sagt Rainer Sigl. Der Blogger und leidenschaftliche Gamer erklärt, warum er sich Blizzards jüngstem Werk verweigert.
Lockheed Martin hat eine neue Version des Exoskeletts Hulc vorgestellt, das es einem Menschen ermöglicht, schwere Lasten zu heben und zu tragen. Der Hersteller will das System im Spätsommer testen und, wenn alles gutgeht, danach an US-Soldaten in Afghanistan ausliefern.
Ein britisches Blog will erfahren haben, dass Facebook den norwegischen Browserhersteller Opera Software kaufen will. Beide Unternehmen wollen sich dazu nicht äußern.
Am 26. Mai 2012 treten neue Datenschutzregeln der EU in Kraft. Websitebetreiber und Werbenetzwerke müssen Nutzer um Erlaubnis fragen, wenn sie Cookies setzen.
Libreoffice könne mehr als Openoffice und biete Entwicklern zudem Vorteile, sagte Michael Meeks auf dem Linuxtag 2012. Außerdem spricht er mit Golem.de über Libreoffice-Online, woran er derzeit arbeitet.