Finalmente in edicola il mio articoletto introduttivo a Ruby on Rails su Linux & C.! Chiaro che non c’è nulla di sconvolgentemente nuovo, ma è conciso e in italiano. E sono particolarmente contento di pubblicare su Linux & C., perché è un’ottima rivista.
Leggo ora una nota di Dijkstra segnalata da un post di Carlo Pescio: My recollections of operating systems design. Ci sono un paio di cose che mi sembrano molto interessanti.
Parlando del famoso algoritmo di Dekker, la prima soluzione corretta al problema della mutua esclusione, Dijkstra dice che da parecchio tempo stava sfidando i suoi colleghi perché producessero una soluzione. Quando la difficoltà di trovare gli errori nelle soluzioni proposte divenne eccessiva, D. cambiò le regole del gioco, richiedendo che insieme all’algoritmo venisse proposta anche una prova di correttezza.
And then something profound and lovely happened. By analyzing by what structure of argument the proof obligations could be met, the numerical mathematician Th.J. Dekker designed within a few hours the above solution together with its correctness argument, and this settled the contest.
L’idea della derivazione di programmi è di fare guidare la soluzione dalla dimostrazione di correttezza. E’ una cosa analoga (non equivalente! ma certamente analoga) a quello che si fa in TDD, dove si fa guidare la soluzione dai test che dimostrano empiricamente che la soluzione funziona.
Ci sono profonde differenze, è ovvio, fra “program derivation” e “TDD”. Ma ci sono anche ovvie analogie: entrambe le tecniche producono programmi molto concisi e corretti. Ed entrambe le tecniche sono molto più efficaci del code & fix, che è la maniera più comune di sviluppare.
A questo proposito D. cita un’episodio divertente:
When the design of the THE Multiprogramming System neared its completion, the University’s EL X8 was getting installed, but it had not been paid yet, and we hardly had access to it because the manufacturer had to put it to the disposal of an American software house that was supposed to write a COBOL implementation for the EL X8. They were program testing all the time, and we let it be known that if occasionally we could have the virgin machine for a few minutes, we would appreciate it. They were nice guys, and a few times per week we would get an opportunity for our next test run. We would enter the machine room with a small roll of punched paper tape, and a few minutes later we would leave the machine room with the output we wanted. I remember it vividly because when they realized what we were achieving, our minimal usage of the machine became more and more frustrating for them. I don’t think their COBOL implementation was ever completed.
Come riesco a immaginarmeli questi sfortunati programmatori… Accanirsi nel code & fix non serve se non si ha un’idea chiara di quello che si sta facendo. Va detto che nei primi anni ’60 scrivere un compilatore era un’impresa un bel po’ più difficile di oggi. Non potevano andarsi a comprare il Dragon Book, perché non era ancora stato scritto!