OT Programmazione - rolling release - chunk 1 2015

[Scara95]

Tutto l'apparato di formalismi è utile per un po' di roba strettamente collegata al mondo matematico. Ad esempio le dimostrazioni di correttezza attraverso i dependet type. Fai qualche ricerca se ti va.

[M.A.W. 1968]

Tutto l'apparato di formalismi è utile per un po' di roba strettamente collegata al mondo matematico. Ad esempio le dimostrazioni di correttezza attraverso i dependet type. Fai qualche ricerca se ti va.

Come già ricordato numerose volte in varie sedi, fin dagli anni Ottanta J e il suo progenitore APL sono di gran lunga i miei linguaggi non convenzionali preferiti, ai quali si sono poi aggiunti B-Prolog (per ovvi motivi!) e Haskell. Si tratta di uno dei linguaggi più divertenti ed intelligentemente concepiti in circolazione.

Non solo: si tratta del linguaggio esotico che uso in assoluto più spesso in ambito professionale, sempre accanto a B-Prolog.
Da quando è stata promulgata la RTCA DO-330 e in particolare l'attesissima appendice DO-333 che per la prima volta standardizza e ufficializza l'uso e l'applicazione dei metodi formali sui quali ho speso gli scorsi venticinque di studio-ricerca-applicazione, i certificatori internazionali hanno dimostrato di approvare largamente (oltre alle ovvietà più lapalissiane, ossia l'output dei soliti Polyspace e AbsInt e le solite paccate di dichiarazioni in Z e/o OCL) anche il theorem proving prodotto con J, B-prolog e loro immediate derivazioni.

Come immediata conseguenza dell'uscita della DO-333 il fenomeno della elevazione delle specifiche (in questo caso la richiesta contrattuale di una specifica avionica anche per applicazioni normate da altre convezioni internazionali) è aumentato del 15% in un semestre. Il mondo industriale, come sostengo da sempre, ha fame di affidabilità e i metodi formali sono una parte essenziale della risposta. In un quarto di secolo è stato recepita normativamente l'essenzialità del loro uso nella specifica, progettazione e verifica dei sistemi massimamente critici: tra una ventina d'anni, magari, lo capiranno anche gli estensori dei piani di studio accademici italiani.

Come ulteriore conseguenza dell'aumentata richiesta di expertise, il tempo libero del sottoscritto tende ormai a zero, così come il numero di interventi sui vari forum.