Buongiorno Giacomo, Giacomo Tesio <giacomo@tesio.it> writes:
Rispetto alle considerazioni di Giovanni (che condivido) ho solo una piccola obiezione:
On Saturday, 15 February 2020, Giovanni Biscuolo <g@xelera.eu> wrote:
il problemone nel caso specifico di SyRI, così come di tutti i sistemi basati su algoritmi *segreti* di profilazione (pubblici e privati), è che **non possono essere fornite sufficienti garanzie**: punto.
Il problema è che questa affermazione non viene mai considerata in tutta la sua serietà.
credo che l'incontro tra tecnici e umanisti stia cominciando a mostrare un percorso su come uscire da questa imbarazzante situazione :-)
solo sistemi basati su algoritmi pubblici, consultabili (e quindi contestabili) forniscono adeguate garanzie costituzionali; solo il software libero garantisce che l'implementazione sia confrontabile con l'algoritmo :-)
E come? :-)
*non* certo con sistemi di verifica formale automatica :-O la verifica algoritmo -> codice sorgente va fatta "a manina", con tanta *arte* da parte di persone con adeguate competeze ed alle quali siano fornite adeguate risorse; aggiungo che a chiunque deve essere data la possibilità di dotarsi di ageguate competenze in merito, in modo tale da poter avere almeno la possibilità di accedere alle risorse i metodi formali [1] (mathematically rigorous techniques for the specification, development and verification of software and hardware systems) *forse* saranno applicabili tra decenni, ma nel frattempo occorre mettere a posto le cose (altrimenti anche i metodi formali non vedranno mai la luce... ma non voglio andare OT)
Quale versione? Su quale sistema operativo? Su quale hardware? Con quali dati in input? Quali valori pseudocasuali sono stati inclusi?
ho l'impressione che tu ti stia riferendo alla verifica di algoritmo, codice sorgente e codice macchina tutto assieme: per ragionare sui metodi di verifica applicabili a ciascuno dobbiamo separare le cose e applicare criteri specifici
Con quali bug?
mi pare di aver già letto altrove il tuo ragionamento attorno ai bug (ma la memoria è ingannevole), diciamo che sarebbe già un enorme passo avanti poter eliminare i bug introdotti nel processo umano di traduzione "algoritmo -> codice sorgente" su quelli resi possibili da certe "indesiderabili caratteristiche" di alcuni linguaggi di programmazione ci si può lavorare (magari cambiando linguaggio di programmazione) ma probabilmente rappresentano il 20% degli effettivi bug... e non entrerei qui troppo nel tecnico detto in altre parole: molti bug (non posso dare numeri, sorry) dipendono da cattiva implementazione delle specifiche
Disporre dei sorgenti di un software è condizione necessaria per spiegarne l'output, ma non è lontanamente sufficiente.
la cosa comincia a farsi un po' tecnica :-) ...però non capisco esattamente a cosa ti riferisci
Di conseguenza, l'introduzione di automatismi non interpretati da menti umane (e dunque non responsabili e irresponsabili) altera in modo inevitabilmente opaco il sistema in cui avviene.
stai parlando con uno che ammira in modo estasiato progetti come stage0 [2] e GNU mes [3], il cui obbiettivo è quello di risolvere una buona volta per tutte il famigerato problema del Trusting Trust [4], che è quello che rende insostenibilmente opaco il mondo del software :-D una breve intro del contesto al quale mi riferisco è la pagina principale del progetto http://bootstrappable.org/: --8<---------------cut here---------------start------------->8--- Do you know how to make yoghurt? The first step is to add yoghurt to milk! How can you build a compiler like GCC? The first step is to get a compiler that can compile the compiler. --8<---------------cut here---------------end--------------->8--- per capirci, l'autore di stage0 scrive (traduzione mia da [2]): --8<---------------cut here---------------start------------->8--- [stage0] ha solo lo scopo di creare un percorso di bootstrapping di un compilatore C in grado di compilare GCC, con il solo requisito esplicito di un singolo binario di 1KByte o meno. In aggiunta, tutto il codice deve poter essere compreso dal 70% della popolazione dei programmatori. Se il codice non è compreso da quella percentuale, occorre modificarlo finché non soddisferà il requisito specificato. --8<---------------cut here---------------end--------------->8--- mi piace pensare a stage0 come al Big Bang dell'universo digitale, con la spettacolare caratteristica che il Big Bang si può ripetere e ispezionare :-D ora, ammetto che ad un primo (e anche secondo) impatto queste cose suonano lunari ai più... ma la sostanza è che alla base di tutta la catena di generazione **e verifica** del software ci sono sempre esseri umani (anche i metodi formali verrebbero applicati *dopo* e "solo" come ausilio al lavoro di analisi umana)
Non si tratta di una cessione di potere "alle macchine" ma certamente si tratta di una sottrazione di tale potere alla comunità umana (a vantaggio di colori che controllano tali automatismi).
la soluzione a tutto questo non è meno informatica, ma informatica migliore :-D
Tuttavia, una volta insediati, tali automatismi sono quasi impossibili da estirpare (prova ne siano gli AS400 che ancora gestiscono nodi cruciali ed insospettabili della vita di moltissime grandi aziende bancarie, assicurative etc...).
eh sì, "Huston abbiamo un problema" :-)
Perché una volta posti in essere, questi impongono ineluttabilmente se stessi e gli esseri umani ne interiorizzano e talvolta persino razionalizzano il funzionamento.
è vero, questo è un problema serio... per questo esistono quei rompiscatole di hackers :-O detto in termini para-filosofici: quello che stiamo osservando non è "la cosa in sé", è un suo fenomeno [...] ciao, Giovanni [1] https://en.wikipedia.org/wiki/Formal_methods [2] https://github.com/oriansj/stage0#goal [3] https://www.gnu.org/software/mes/ [4] https://en.wikipedia.org/wiki/Backdoor_(computing)#Compiler_backdoors -- Giovanni Biscuolo Xelera IT Infrastructures