[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [FYI] Ross Anderson - Open and closed security are roughly equivalent



* Martin Uecker wrote:
>>> Aber selbst dann wird man für komplexe Programmsysteme, die in
>>> imperativen Sprachen geschrieben sind, niemals irgenwelche
>>> komplizierten Eigenschaften beweisen können.
>>
>> Beweis durch Behauptung? Warum klappt das dann in den o.g. Beispielen?
> 
> Weil das keine komplizierten Eigenschaften sind. Halbwegs kompliziert
> wäre z.B. die Implementation eines Filesystems darauf zu testen, ob
> die Datenstrukturen auf der Platte immer konsistent bleiben.

Ich halte fest: Hubschraubersteuerungen und CA-Systeme nicht trivial im
Vergleich zu Filesystemen. Man lernt auf debate immer dazu.

>> Spark geht noch weiter und prüft die Imperativen Statements, den
>> Informations- und Datenfluß und einige kleine Stilfragen.
>
> Formal logische Aussagen sind isomorph zu Typen. Ein Verifikationstool
> kann deswegen auch nicht mehr, als was man in geeigneten Sprachen mit
> Typen machen kann.

Ich kann Dir gerade nicht folgen. Wie beweist man durch Angabe eines
(skalaren) Typs, daß in dem Ausdruck "4*len/3" kein Überlauf auftritt?
Bitte per eMail, für debate ist das zu speziell.

> Das Problem ist, daß automatische Beweiser bei imperativen Sprachen nicht
> wirklich weit kommen. Seiteneffektfreie Sprachen sind ja gerade aus
> diesem Grund auf diesem Gebiet so beliebt.

Seiteneffektfreiheit kann mit mit Datenflußanalyse zeigen. Es ist nicht
notwendig, daß alle Sprachkonstrukte diese Eigenschaft haben. Und man spart
sich die Monade der Welt.

-- 
To unsubscribe, e-mail: debate-unsubscribe@lists.fitug.de
For additional commands, e-mail: debate-help@lists.fitug.de