Correctnes by construction

[Saarländer]

Beweisen ist ein paar Zehnerpotenzen schneller als früher.
Moores Law sei Dank.

"Der falsche Glaube an die exponentielle Fehlerzunahme hat die VLSI-Technologie 10 Jahre verzögert". Wir könnten die Chips von in 10 Jahren schon heute haben !

Beweisen ist möglich.
Der Trick ist nicht, jeden cripple-crap-PHP-Code beweisen zu wollen.
Der Trick ist: Du kriegst den Auftrag nur, wenn Du bewiesenen Code ablieferst inclusive Beweisen und Logs und Traces usw.
D.h. Du programmierst gleich Beweiserfreundlich. Damit wird Gödel zur Legende. Denn ich brauche und will gar nicht jeden Code beweisen. Sondern ich bestelle bewiesenen Code bei der Ausschreibung. har har har.

Sowas was Statiker jeden Tag bei Gebäuden und Brücken machen und durchrechnen. Halt bei Software.

Auch beweist man verschiedene Dinge. Und zwar je nachdem, was man braucht. Maximaler Speicherplatz bei Bloat-Fox, maximale Stacktiefe, Anzahl der TCP-Connects.
Anzahl der SMS, die man braucht, um eine Feuerwehr-wagen-Meldung an die Feuerwehr-Zentrale zu senden.
Anzahl und Dauer des Kommunikation zum Mars usw.
Unanfälligkeit gegen Buffer-Overflows usw.

[IT-Kunstentdecker]

Du schreibst wie er!

[Oaktrail]

Das 4augen-Prinzip oft nicht Leistung liefert, hast Du ein paar Golem-Meldungen höher bei "lex-linux's lame" lesen dürfen.

Und das man besser anständig planen soll, kann man im Forum auch lesen.

[Der Blub]

Jaja Gödel wird nicht zur Legende, Gödel ist legendär...
Man siga, hol dir ein gutes Buch über theoretische Informatik und dann wirst du vielleicht im Ansatz merken, was für ein Stuss du laberst

[IT-Kunstentdecker]

Was? Ô_ó

[Saarländer]

Bei Dächern und Wintergärten "beweist" Du statisch (nicht statiSTIsch), das sie Schnee-Lasten von z.b. 120 kg/m^2 vertragen.

Und man "beweist" z.B. das Wind-lasten bei XX km/h bei z.b. UMTS-Antenne ohne das die Antenne in die Innenstadt fliegt und Leute zermatscht oder abgerissene Teile Fußgängern Körperteile rausfetzen oder halt Autos beschädigen.

Eine Sat-Schüssel darf man dann bald wegen Versicherung nicht mehr anbringen. Weil die Orkantornados durch Klima-Erwärmung sie sowieso bald abreissen werden.

Ich glaube, Du solltest erst mal Gödel verstehen.

Man kann automatisch nicht ALLE Programme beweisen.
Das heisst aber nicht, das man keine bewiesene Software abliefern kann. Wenn Du eine Vorlesung besucht hast, wüsstest Du genug Beispiele wo krass stundenlang bewiesen wurde. Oft nur Laufzeit. Manchmal Korrektheit. Halt nicht automatisch. Aber ALGORITHMEN (nicht Programme) muss man sowieso (mit der Hand selber) beweisen.
Du schreibst dann also Software, wo der Software-Beweiser mit klar kommt.
Probleme gibts dann damit, was überhaupt bewiesen werden soll. Das ist aber erst mal ein anderes Problem. Nämlich ein Spezifikations-Fehler.

Das ist wie Einstein. Da haben manche Leute nämlich die falsche Vorstellung, das Impuls und Materie(?) oder was auch immer nicht schneller als Lichtgeschwindigkeit gehen. Eines davon geht aber schneller. Das andere geht halt nicht schneller, weil Lichtgeschwindigkeit die Grenze ist und man endlos Energie bräuchte. Ich glaube, Heise hatte das mal erwähnt.

Und noch was: Die meisten Sprachen sind z.B. LALR(1) weil die Parser sonst zu aufwendig werden.
Das heisst aber nicht, das man keine LALR(2)- oder LL(2)-Programme schreiben kann. Man muss dann dem Compiler halt "Tipps" geben. Bei .NET geht das vielleicht nicht. Aber bei Java gibts Annotationen. Damit ginge das. Bei Java ist das natürlich nicht nötig. Aber es könnte ja mal Konfigurations- oder Computer-Sprachen geben, wo man dadurch übersichtlicheren Code hin bekäme und es einem das wert wäre.

Aber solche Themen sind natürlich nur für Leute, die wirklich Theorie-Vorlesungen besucht haben. Die anderen heulen gleich rum das sie zu dumm sind.

Ein Stealth-Fighter schickt fast keine Radarstrahlen zurück. Aber es strahlt sie an die Umgebung ab.
Ein Radargerät pingt in die Richtung vom Fighter(weil es sich dreht also überall hin) und das zweite Radargerät kriegt die zerstreuten Signale. TV-Bericht: "Die neuen kleinen Antennen auf den Radaranlagen weisen auf die neue Vernetzgung von Radarstationen gegen Stealth-Fighter hin".
Und so ein Inder meinte: Mit meinem tollen Wetter-Radar (deutsche Radarstation) sehe ich den Stealhfighter auch am Kondenswasser.

Ein optisches Gerät kann nicht feiner auflösen als die Wellenlänge oder sowas. Das krasse Super-Mikroskop wofür evtl. ein Deutscher (IBM Schweiz?) den Nobelpreis bekommen hat, arbeitet daher mit ZWEI UNABHÄNGIGEN Optischen Messgeräten und kann dadurch feiner "schauen" als die Wellenlänge womit es arbeiten muss.

Lern es endlich: Physikalische Probleme umgeht man, wenn einem ein Weg einfällt.
Und bei Gödel geht das auch.

Du baust Dir ja keine Flügel an die Arme.
Du beschleunigst einen Auftriebs-Körper (Flugzeug-Flügel) indem Du volle Kanne vorwärts fährst, und dadurch die Mühle hochkommt. "Das ist doch voll dumm. Nach vorne fahren damit ich hoch komme. Ich glaube nicht an Flugzeuge."

Oder halt die Flügel schnell um eine Achse drehst und sie Rotoren nennst und die Mühle Hubschrauber.

Leute wie Du hätten sich vielleicht Nerd-Kappen gebaut wo die Propeller oben am Kopf sind und Dich nach oben ziehen sollen... Cessna und die Wright-Brothers hingegen haben die Flügel nach vorne zeigen lassen. Das waren halt keine Dumm-Nerds.

[Wyv]

>>Das heisst aber nicht, das man keine bewiesene Software >>abliefern kann.

Richtig. Aber der Anspruch dadurch nur noch bewiesene Software abzuliefern, ist dadurch trotzdem nicht haltbar. Das wird spätestens bei der Benutzerinteraktion zu einem Problem.

[Saarländer]

Wyv schrieb:
--------------------------------------------------------------------------------
> >>Das heisst aber nicht, das man keine bewiesene Software >>abliefern
> kann.
>
> Richtig. Aber der Anspruch dadurch nur noch bewiesene Software abzuliefern,
> ist dadurch trotzdem nicht haltbar. Das wird spätestens bei der
> Benutzerinteraktion zu einem Problem.

Was soll daran ein Problem sein.
Man beweist, das nur saubere Zustände erreicht werden können.

Wenn benutzte (M$-)Libs unsicher sind, ist das was anderes.
Daher gibts ja diese Vor-Bedingungen.
Die Nachbedingungen sind dann im Prinzip Annotationen, was überhaupt bewiesen werden soll.
Assertions (?). In Eifel ist das üblich. Durch Annotationen in Java wäre das auch mal nett.
Dann könnte man jede zehnte Transaktion mit eingeschalteten Assertions laufen lassen, um zu sehen, ob was schief geht oder eine böse Library falsche Parameter oder unzulässige Daten liefert: "Ich will -5 Waschmaschinen bestellen. Überweis das Geld auf meine Kreditkarte".

Bei User-Daten stellt sich die Frage, ob sie überprüfbar sind. Aber dann ist das u.U. kein informatisches Problem. Z.B. ob jemand seine Bestellung bezahlen kann und anklickt "ich werde bezahlen" kann es ja gelogen sein. Oder Bestell-Nomaden usw.

Bei Fremd-Daten und Fremd-Formaten wie z.b. Bildern in Browsern hat man solche Probleme auch. Seit neuestem auch häufiger mit PDF-Dokumenten. Aber auch sowas sollte auch machbar sein.
Das ist aber eher eine andere Sorte Problem. Bzw. mangelnde Definition und Überprüfung der Vorbedingungen.

Korrektur im letzten Absatz:
Falsch: "Flügel nach vorne zeigen lassen"
Richtig: "Propeller nach vorne zeigen lassen"

[16Bitiges Bit]

Java hat doch auch Assertions.