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

Re: Ripristino GRUB2 e conversione GPT...



On Mon, Mar 01, 2021 at 06:37:13PM +0100, Marco Bodrato wrote:
> Saluton, Marco!
> 
> Il 2021-03-01 17:31 Marco Ciampa ha scritto:
> > On Sat, Feb 27, 2021 at 01:55:15AM +0100, Sabrewolf wrote:
> 
> > NESSUN tool, né commerciale né libero, garantisce al 100% la riuscita
> > dell'operazione. Equivarrebbe a dire che il sw è senza alcun baco, cosa
> > che è dimostrabile matematicamente che è impossibile.
> 
> Questa frase non si capisce tanto :-)
> 
> Probabilmente si può dimostrare matematicamente che esistono programmi la
> cui correttezza non è dimostrabile, "parafrasando" il teorema di Goedel.

ecco, diciamo che lo hai detto meglio ma il "succo" è lo stesso... perdonami
non sono un matematico, sono un praticone / smanettone

> Ti assicuro però che per funzioni sufficientemente specifiche è possibile
> dimostrare matematicamente che fanno esattamente quel che dovrebbero, senza
> bachi.

Questo lo so. So anche che funzioni specifiche non sono programmi.
Sostanzialmente programmi non banali sono impossibili da verificare, per
le cose che dici tu stesso sotto. Questa è una cosa che si sa, anzi che
sanno tutti, non è che stia dicendo una cosa rivoluzionaria.

Tant'è che _tutti_ i programmi hanno una licenza che espressamente toglie
qualsiasi responsabilità per errori.

> 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
implementato? Perché non mi pare che le due cose si equivalgano, ma qui
vado in un campo di cui non so niente per cui potrei dire delle cavolate.

> Va da sé che poi servirebbe anche la verifica formale del compilatore, la
> verifica formale dell'hardware sul quale il software gira... e negli utlimi,
> anni blasonate case produttrici di microprocessori ci hanno purtroppo
> abituato alla sciatteria più vergognosa.

Ahhhh ecco infatti mi pareva che ci fosse "il trucco". Ergo, non si può
mettere la mano sul fuoco su niente... anzi, si può quasi fare il
contrario e scommettere sui problemi...

> Ma tra la grande complessità e l'impossibilità matematica, c'è differenza
> :-D

... c'è differenza ... per un matematico. Per un matematico

0,99999999999999999999999999999999999999999999999999999999999999\
9999999999999999999999999999999999999999999999999999999999999999\
9999999999999999999999999999999999999999999999999999999999999999

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

Diciamo che è molto difficile provare la correttezza formale di un programma.
Contento? ;-)

> Chi in questi anni ha prodotto CPU scadenti, o venduto software con una
> bella confezione, tanta propaganda e poca qualità, non è giustificabile da
> una presunta impossibilità matematica di lavorare bene.

Ma anche no. Ci sono i difetti di fabbricazione, i raggi cosmici, la
radioattività naturale, gli effetti quantici, ecc. ragioni per non avere
la certezza della correttezza ce ne sono a bizzeffe...

Inoltre la complessità computazionale aumenta esponenzialmente la
probabilità di problemi per cui hai quasi la certezza matematica (ho
messo il quasi, ok?) che ci siano problemi. Se la certezza è 1 allora il
mio "quasi" somiglia al numero espresso sopra...

> Che poi errare sia
> umano (e perseverare anche) è cosa che tutti sappiamo, ma non ne facciamo
> una gistificazione matematica o scientifica, che sarebbe altra cosa.

Si ma io sono un _pratico_ e dico che _praticamente_ assumo che i
programmi abbiano bachi, _tutti_ i programmi. Se sbaglio, sbaglio di
poco, molto poco. La differenza con 1 di cui sopra.

> > > Cioè, se non vuoi "perdere i dati" allora significa che sono
> > > importanti e quindi dovresti avere già un backup e quindi anche se
> > > perdi
> > > i dati il problema non si pone :-D
> > 
> > Esatto. Il metodo è: faccio backup, cancello la partizione, la ricreo
> > GPT, ricopio i dati. Questo funziona al 100%, per forza.
> 
> Questo metodo è lento... e non "funziona al 100%, per forza".
> Hai tenuto conto dei bachi del software per fare il backup? Della
> possibilità che il disco di backup sia difettoso?

Certamente e infatti i backup vanno verificati, e la norma 321 dice anche
che bisogna farne almeno due...

> Un metodo più veloce nel caso medio e non troppo più lento nel caso peggiore
> e comunque più sicuro è:
> 
> Faccio il backup (questo è imprescindibile)

ok

> Non cancello i dati, ma uso il software che mi promette di funzionare nella
> maggior parte dei casi per fare la conversione.

se c'è... e se il tempo che perdi a cercare di fare la conversione è
superiore al tempo necessario ad _avviare_ (mica stai li a guardare no?)
il backup, recover e controllo, allora lascia perdere...

> Controllo che tutto sia andato a buon fine, nel qual caso ho risparmiato un
> sacco di tempo. In caso contrario, recupero i dati dal backup direttamente
> nella nuova struttura di disco/partizioni/filesystem.

ok

> È più sicuro, perché si rischia di perdere dati solo nel caso in cui la
> particolare configurazione risveglierà sia un bug nella procedura di
> backup/ripristino, sia in quella di conversione. La probabilità che entrambe
> siano bacate è più bassa della probabilità che anche solo una delle due lo
> sia.

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

> La cosa su cui tutti, mi pare, concordiamo è: fare copie di sicurezza,
> frequentemente e soprattutto (ma non solo) in occasione di operazioni
> delicate.

esattamente

> Ĝis,

Ĝis ;-)

--

Saluton,
Marco Ciampa


Reply to: