datagott > wetenschap

Cohen (11.01.2019, 12:33)
On Fri, 11 Jan 2019 10:20:22 +0000, Izak van Langevelde wrote:

> On Thu, 10 Jan 2019 23:45:51 +0000, Cohen wrote:
>> Dat zal ik zeker doen, al is het maar omdat ik geen bedrijven ken die

> zich daarmee bezighouden.


Verum: <https://www.verum.com/company/>

>> Nutteloos voor iets complexers? Er zijn volledig formeel geverifiveerde
>> kernels. In toepassingen waar fouten grote gevolgen hebben heeft
>> formele verificatie natuurlijk wel degelijk zin.
>> <https://sel4.systems/About/seL4/>

> Daar lees ik niets over Dijkstra. Zonder bewijs is Uw claim nietig.


Het is een standing on the shoulders of giants verhaal maar hij zit erin:

"Finally, as in Dijkstra’s postcondition propagation [7], the
precondition used must be proved to be a consequence of the one that was
originally assumed."

<https://
pdfs.semanticscholar.org/673b/65fe0d2b4b09999b5ab2dbc7dcce98be516b.pdf>
Rob (11.01.2019, 12:37)
Cohen <cohen> wrote:
> On Fri, 11 Jan 2019 08:42:59 +0000, Rob wrote:
>> Dat moge zo zijn maar hoe lager de fout zit, hoe groter de potentiele

> gevolgen.


Nee dat hangt veel meer af van het belang van die specifieke component
en de manier waarop fouten verwerkt worden dan van de laag waar die in zit.

> Dat moge allemaal zo zijn maar het helpt als je een laag kan uitsluiten
> omdat deze aantoonbaar correct is (nou ja, als de specificaties die de
> laag moet vervullen correct zijn).


Als je missie alleen succesvol is als alles correct werkt dan kom je pas
verder als je dat van alle lagen kunt aantonen.
Je kunt ook inzetten op een zodanig design dat je missie ook nog slaagt
als niet alles correct werkt.
Het is echter verleidelijk om daarbij een afweging te maken mbt kosten/moeite
en van te voren bedachte problemen en hun oplossing.
Bijvoorbeeld als een component kan falen, dan deze dubbel of driedubbel
uitvoeren om nog een backup te hebben of zelfs een "majority vote" dat
klinkt leuk maar als die 2 of 3 componenten identiek zijn en het falen
een gevolg is van een ontwerp- of implementatiefout, dan heb je daar
niets aan.
Jos Bergervoet (11.01.2019, 13:06)
On 1/11/2019 11:37 AM, Rob wrote:
> Cohen <cohen> wrote:
>> On Fri, 11 Jan 2019 08:42:59 +0000, Rob wrote:
>>> Cohen <cohen> wrote:
>>>> Euh... Houdt u zich s.v.p. verre van bv. software in kernreactors en
>>>> raketten.


Maar de rest mag natuurlijk wel! (En daar is toch het meeste aan
te verdienen, nietwaar?)

...
> Als je missie alleen succesvol is als alles correct werkt dan kom je pas
> verder als je dat van alle lagen kunt aantonen.
> Je kunt ook inzetten op een zodanig design dat je missie ook nog slaagt
> als niet alles correct werkt.


Of je dwingt de klanten gewoon vooraf te betalen! Dan hoeft het niet
eens te werken (dat is toch in feite de moderne aanpak?! Als het dan
niet werkt is dat juist gunstig, dan moeten ze nog een keer betalen
voor de upgrades. Die domme Dijkstra begreep dat niet..)

> Het is echter verleidelijk om daarbij een afweging te maken mbt kosten/moeite
> en van te voren bedachte problemen en hun oplossing.


Exact! Het moet vooral weinig "moeite" zijn (voor de programmeurs) en
het mag gerust wat kosten (voor de klant!) Da's het juiste "paradigma".
Izak van Langevelde (11.01.2019, 13:07)
On Fri, 11 Jan 2019 10:33:34 +0000, Cohen wrote:

> On Fri, 11 Jan 2019 10:20:22 +0000, Izak van Langevelde wrote:
>> Verum: <https://www.verum.com/company/>
>> Het is een standing on the shoulders of giants verhaal maar hij zit

> erin:
> "Finally, as in Dijkstra’s postcondition propagation [7], the
> precondition used must be proved to be a consequence of the one that was
> originally assumed."


Dat is een zwaktebod: dat er een notie van Dijkstra wordt gebruikt, maakt
het nog geen bewijs cf. Dijkstra.

> <https://
> pdfs.semanticscholar.org/673b/65fe0d2b4b09999b5ab2dbc7dcce98be516b.pdf>


Dat is volledig academisch werk, die jongens moeten publiceren en hebben
helemaal geen tijd aan een serieuze kernel te werken. Bovendien lees ik
"The proof assumes correctness of compiler, assembly code and hardware.
It also assumes correct use of low-level hardware caches (memory caches
and translation-look-aside buffer) and correctness of the boot code",
hetgeen betekent dat het werk niets over de betrouwbaarheid van de kernel
zegt.
Cohen (11.01.2019, 13:18)
On Fri, 11 Jan 2019 11:07:09 +0000, Izak van Langevelde wrote:

> On Fri, 11 Jan 2019 10:33:34 +0000, Cohen wrote:
>> Dat is een zwaktebod: dat er een notie van Dijkstra wordt gebruikt,

> maakt het nog geen bewijs cf. Dijkstra.
>> Dat is volledig academisch werk, die jongens moeten publiceren en hebben

> helemaal geen tijd aan een serieuze kernel te werken.


<https://docs.sel4.systems/GettingStarted>

> Bovendien lees ik
> "The proof assumes correctness of compiler, assembly code and hardware.
> It also assumes correct use of low-level hardware caches (memory caches
> and translation-look-aside buffer) and correctness of the boot code",
> hetgeen betekent dat het werk niets over de betrouwbaarheid van de
> kernel zegt.


Kan je nagaan hoe erg het bij een reguliere kernel is.
Johan Wevers (11.01.2019, 19:05)
On 10-01-2019 23:20, Jos Bergervoet wrote:

> expressie," niks control flow! Je denkt toch niet dat er een "program
> counter" is waar dat DNA zich dan ook nog iets van aan zou trekken?


Nou ben ik geen geneticus, maar VZIW kan een gen niet twee maal tegelijk
tot expressie worden gebracht omdat ribosomen de boel bezet houden tot
de vertaling naar RNA klaar is. Ik las in elk geval wel eens iets dat
men in bepaalde gewassen de concentratie van bepaalde eiwitten wilde
verhogen door hetzelfde gen meerdere malen in het genoom te zetten. Code
duplicatie is programmeertermen, considered bad practice.

> Exact wat ik bedoel. Is er in de genetica ooit ook maar n zo'n
> correctheidsbewijs geleverd?!


Als het te slecht is gaat het organisme vanzelf dood.
Johan Wevers (11.01.2019, 19:06)
On 11-01-2019 0:45, Cohen wrote:

> Nutteloos voor iets complexers? Er zijn volledig formeel geverifiveerde
> kernels. In toepassingen waar fouten grote gevolgen hebben heeft formele
> verificatie natuurlijk wel degelijk zin.


Ja, in vliegtuigen bijvoorbeeld. Zie de F35 JSF voor een fraai voorbeeld...
Johan Wevers (11.01.2019, 19:09)
On 11-01-2019 12:06, Jos Bergervoet wrote:

> Exact! Het moet vooral weinig "moeite" zijn (voor de programmeurs) en
> het mag gerust wat kosten (voor de klant!) Da's het juiste "paradigma".


Je kunt er twee kiezen uit goed, snel en goedkoop. Alle 3 tegelijk gaat
niet lukken.
Rob Windgassen (11.01.2019, 20:29)
On Fri, 11 Jan 2019 10:20:22 +0000, Izak van Langevelde wrote:

> On Thu, 10 Jan 2019 23:45:51 +0000, Cohen wrote:


>> Euh... Houdt u zich s.v.p. verre van bv. software in kernreactors en
>> raketten.

> Dat zal ik zeker doen, al is het maar omdat ik geen bedrijven ken die
> zich daarmee bezighouden.


bedrijven niet kennen is niet voldoende, van te voren wisten ze ook niet
waar stuxnet de kop op zou steken.

[..]
Izak van Langevelde (11.01.2019, 21:21)
On Fri, 11 Jan 2019 18:29:28 +0000, Rob Windgassen wrote:

> On Fri, 11 Jan 2019 10:20:22 +0000, Izak van Langevelde wrote:
>> bedrijven niet kennen is niet voldoende, van te voren wisten ze ook niet

> waar stuxnet de kop op zou steken.
> [..]


Laat ik het zo zeggen, we hebben in Nederland geen software industrie van
enige betekenis, men vind het al heel innovatief om een database aan het
web te hangen.
het varken uit Stettin (11.01.2019, 21:30)
On 11-01-19 20:21, Izak van Langevelde wrote:
> On Fri, 11 Jan 2019 18:29:28 +0000, Rob Windgassen wrote:
>> Laat ik het zo zeggen, we hebben in Nederland geen software industrie van

> enige betekenis, men vind het al heel innovatief om een database aan het
> web te hangen.


Maar men vraagt daar dan wel enkele tientallen miljoenen voor... In het
eerste decennium van deze eeuw werkte ik ergens waar ik daar inzicht in
kreeg. De corruptie, de schraapzucht en de onwetendheid..!

Het automatiseringsbedrijf in kwestie had de bijnaam 'de rose olifant'
en dat had niets met drank te maken. O ja, en denk maar niet dat daar de
eerstkomende tien, twintig jaar openheid van zaken over wordt gegeven -
ze hebben er ook hele goede advocaten.
Izak van Langevelde (11.01.2019, 21:54)
On Fri, 11 Jan 2019 20:30:08 +0100, het varken uit Stettin wrote:

> On 11-01-19 20:21, Izak van Langevelde wrote:
> Maar men vraagt daar dan wel enkele tientallen miljoenen voor... In het
> eerste decennium van deze eeuw werkte ik ergens waar ik daar inzicht in
> kreeg. De corruptie, de schraapzucht en de onwetendheid..!


Die jongens investeren echt niet in spftware kwaliteit...
Rob Windgassen (11.01.2019, 22:10)
On Fri, 11 Jan 2019 19:21:21 +0000, Izak van Langevelde wrote:

> On Fri, 11 Jan 2019 18:29:28 +0000, Rob Windgassen wrote:
>> Laat ik het zo zeggen, we hebben in Nederland geen software industrie van

> enige betekenis, men vind het al heel innovatief om een database aan het
> web te hangen.


Is ook niet nodig. Ook kerncentrale en raketten worden gebouwd met componenten
van kleinere leveranciers.
Jos Bergervoet (12.01.2019, 00:09)
On 1/11/2019 12:07 PM, Izak van Langevelde wrote:
> On Fri, 11 Jan 2019 10:33:34 +0000, Cohen wrote: ...
>> <https://
>> pdfs.semanticscholar.org/673b/65fe0d2b4b09999b5ab2dbc7dcce98be516b.pdf>

> Dat is volledig academisch werk, die jongens moeten publiceren en hebben
> helemaal geen tijd aan een serieuze kernel te werken. Bovendien lees ik
> "The proof assumes correctness of compiler, assembly code and hardware.


Ja, prima toch? "Bewijs teruggebracht tot eerder bewezebn stelling!"

Offeu.. gebruik jij compilers die niet bewezen correct zijn? En dan
zeker hardware waar die overgestempelde afgekeurde chips in zitten?!

> It also assumes correct use of low-level hardware caches (memory caches
> and translation-look-aside buffer) and correctness of the boot code",


Om nu terug te keren tot dat DNA: we veronderstellen natuurlijk ook
dat de aminozuren daarin volledig aan de specs voldoen. En dat de
electronen en protonen die erin zitten foutenvrij zijn en stuk voor
stuk uitwisselbaar. (Foute electronen komen de Hilbertruimte niet eens
binnen. De creatieoperatoren leveren alleen perfect werk!

<https://en.wikipedia.org/wiki/Creation_and_annihilation_operators#Creation_and_a nnihilation_operators_in_quantum_field_theories>)
Jos Bergervoet (12.01.2019, 00:22)
On 1/11/2019 6:05 PM, Johan Wevers wrote:
> On 10-01-2019 23:20, Jos Bergervoet wrote:
>> expressie," niks control flow! Je denkt toch niet dat er een "program
>> counter" is waar dat DNA zich dan ook nog iets van aan zou trekken?

> Nou ben ik geen geneticus, maar VZIW kan een gen niet twee maal tegelijk
> tot expressie worden gebracht omdat ribosomen de boel bezet houden tot
> de vertaling naar RNA klaar is.


Maar een centraal geleide control is er toch niet, het is een vrij
autonome bedoening daar in die kern!

> Ik las in elk geval wel eens iets dat
> men in bepaalde gewassen de concentratie van bepaalde eiwitten wilde
> verhogen door hetzelfde gen meerdere malen in het genoom te zetten. Code
> duplicatie is programmeertermen, considered bad practice.


In de broncode, ja, maar niet in de machinecode! Loop-unrolling is
een van de standaard-optimalisatieklussen waar de compiler de winst
uit haalt.

>> Exact wat ik bedoel. Is er in de genetica ooit ook maar n zo'n
>> correctheidsbewijs geleverd?!

> Als het te slecht is gaat het organisme vanzelf dood.


Welnee, je hebt speciale diagnose-organismen, die bij fouten in
een ander organisme geactiveerd worden en dan een patch uitvoeren
(na eerst een zeer zorgvuldige diff, natuurlijk!). Slechts in heel
weinig gevallen is er tegenwoordig nog een core dump nodig met
een post-mortem analyse.

Soortgelijke onderwerpen