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

Verifiche formali di programmi [era: Ripristino GRUB2 e conversione GPT...]



Saluton Marco,

Il 2021-03-01 19:37 Marco Ciampa ha scritto:
ecco, diciamo che lo hai detto meglio ma il "succo" è lo stesso... perdonami

Non proprio lo stesso...
È un po' come la differenza tra "in Italia ci sono dei mafiosi" e "gli italiani sono tutti mafiosi". Il non distinguere tra le due di solito porta a gravi conseguenze :-P
...e non solo parlando di Italia e di mafia.

Per fare un esempio che potrebbe non interessare molte persone, ma che
affascina enormemente me, c'è un'intera libreria di calcolo matematico in
precisione arbitraria che è formalmente verificata:
https://gitlab.inria.fr/why3/whymp

Interessante. Domanda da profano: verifica formale equivale ad assenza di
bachi o semplicemente indica che quello che viene descritto
nell'algoritmo (che potrebbe avere dei problemi) viene correttamente

Per fare un esempio interno alla libreria citata, la verifica formale fatta dagli autori (pubblicata e riproducibile) di una funzione come "radice quadrata intera di un intero" garantisce che la funzione non legga/scriva in aree di memoria diverse da quelle in cui può leggere/scrivere. Garantisce anche che per qualunque intero "arbitrariamente" lungo x fornito come argomento, venga fornito nel formato atteso un risultato r tale che r^2 <= x < (r+1)^2.

Certo, se qualcuno usa la funzione powm per l'esponenziazione modulare da quella libreria e ci costruisce sopra della crittografia RSA; la libreria garantirà che le potenze-modulo diano il risultato matematicamente corretto partendo da quel che le verrà dato in pasto. Se pero il programma che usa la libreria è sbagliato o la crittografia RSA non è sicura, non sarà l'uso di una libreria formalmente verificata ad eliminare questi problemi.

Perché questa chiacchierata non scivoli troppo nel fuori luogo (Off Topic), l'infrastruttura di programmi che serve per verificare queste dimostrazioni è presente in Debian, nel pacchetto why3 https://packages.debian.org/source/sid/why3

Un primo germe della libreria che ho indicato è presente nel pacchetto why3-examples ed una volta installatolo si trova in
/usr/share/doc/why3-examples/examples/multiprecision

Per un matematico

0,99999999999999999999999999999999999999999999999999999999999999\
9999999999999999999999999999999999999999999999999999999999999999\
9999999999999999999999999999999999999999999999999999999999999999

è completamente diverso da 1. Dillo ad una cassiera del supermercato e
sta pronto ad abbassare la testa... ;-)

Prova a dirlo tu alla stessa persona che invece di digitare 1 sulla cassa può tranquillamente scrivere 0 seguito dalla sfilza di 9 che hai proposto, oppure prova a dirlo ad una tipografa che quelle tre righe di 9 sono la stessa cosa di un singolo "1" e vedrai che le opinioni in proposito sono più variegate di quelle che ti aspettavi :-)

Poi suvvia, sono sicuro che esistano anche cassiere del supermercato acculturate, capaci di cogliere le sottigliezze, come chessò... la differenza tra software libero e software gratuito! E se per caso la capacità di discernere non è sufficientemente diffusa, bene adoperiamoci perché lo sia!

vedi che anche tu guardi le probabilità e non le certezze matematiche?

L'importante è non confonderle!

Ĝis,
m


Reply to: