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.
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.
"Quid enim est, quod contra vim sine vi fieri possit?" - Cicerone, Ad Familiares
Interessante come riesci a creare faccine che fanno effettivamente qualcosa di utile.
Ad esempio (>-<)
"Quid enim est, quod contra vim sine vi fieri possit?" - Cicerone, Ad Familiares
oggi ho letto un articolo cu cython.
sembra interessante, ma mi sorge subito una domanda: perchè non usare direttamente c/c++ a quel punto?
qualcuno di voi ha esperienza in materia?
Uhm, in che linguaggio?Originariamente inviata da Scara95
Comunque, mi hai fatto venire in mente il gustoso idioma dell'"operatore freccia":
codice:for(int i=10; i-->0;) // Leggi "i va a zero" printf("%d", i);Non l'ho mai usato direttamente, ma l'hanno usato in un nostro prodotto per motivi di performance, credo che sia un po' più comodo da integrare (e sia più leggibile) rispetto alle alternative per la creazione di binding C/C++ - Python. Usiamo spesso SIP per creare binding Python-C++, e ti posso assicurare che non è assolutamente un piacere da usare.
Amaro C++, il gusto pieno dell'undefined behavior.
in j, ma puoi farne di cose strane. Quella è una funzione compare. Una chiamata x (>-<) y equivale a (x>y)-(x<y) che altro non fa che comparare due numeri e restituire 1 0 o _1.Uhm, in che linguaggio?
Comunque, mi hai fatto venire in mente il gustoso idioma dell'"operatore freccia":
codice:for(int i=10; i-->0;) // Leggi "i va a zero" printf("%d", i);
Analoga è la definizione di media che danno sempre per sfoggiare il linguaggio +/ % #
/ (insert) inserisce l'operatore fra gli elementi dell'array, # conta gli elementi. Una chiamata (+/ % #) y è interpretata come (+/ y) % (# y)
Il punto comunque non era come funziona, era che facendo codegolf alla fine guardi ciò che hai ottenuto e vedi una fila di simboli a caso con in mezzo emoticon random .-.
"Quid enim est, quod contra vim sine vi fieri possit?" - Cicerone, Ad Familiares
Ma quanto è potente l'ILP (Instruction-Level Parallelism)? Cioè, l'accumulazione in una variabile è più veloce (3x) se fatta per somme parziali perché permette alla CPU di eseguire le addizioni in parallelo, cosa non possibile senza le variabli ausiliarie. Questo dimostra quanto sia difficile al giorno d'oggi ottenere il massimo throughput.
Che ne pensate di Rust?
Era uno dei motivi per cui pensavo di imparare qualcosina di SSE e compari, anche se anche i compilatori ci stanno arrivando (ogni tanto vedo del codice generato da gcc recenti con vettorizzazione automatica che fa paura... certo, fino a qualche tempo fa ogni tanto faceva anche delle cagate apocalittiche).
L'ho guardato un po' di tempo fa, secondo me è un passo nella direzione sbagliata. Mi sembra che per rincorrere un ideale di gestione di lifetime "garantito corretto" ma senza ricorrere a sistemi di garbage collection stiano inserendo una serie di complicazioni e sovrastrutture assurde a livello di type system e di uso concreto del linguaggio... mi sembra una visione troppo "da vicino" del problema dell'ownership (per cui si "istituzionalizzano" dentro al linguaggio certe pratiche), che non considera che uno quando scrive codice non è che vuole una sintassi più bella per gestire la memoria, vuole semplicemente dimenticarsi di tutte queste menate e occuparsi del problema vero su cui sta lavorando.Che ne pensate di Rust?
Amaro C++, il gusto pieno dell'undefined behavior.
È quello che ti da potenza se lo usi bene, ma ti da di quelle smazzate sennò. Pensa quanto sono diventate imprevedibili le CPU di oggi per sfruttare l'ILP: pipeline profonde, branch prediction, esecuzione ahead of time, ...
Tutte belle cose che ti danno potenza quando ci indovinano, ma se c'è qualcosa che gli fa un ' dispetto' è una mazzata. Diventa sempre più difficile prevede le tempistiche.
Le istruzioni SIMD sono un discorso affine ma non direttamente collegato.
"Quid enim est, quod contra vim sine vi fieri possit?" - Cicerone, Ad Familiares
Il discorso è che un compilatore è uno strumento con potenzialità limitate. Molto limitate. Nell'esempio che ho prima fatto, nessun compilatore è in grado di ottimizzarlo (forse alcune direttive specifiche potrebbero aiutarlo) perché, per quanto penso, si tratta comunque di qualcosa dipendente da architettura ad architettura.Era uno dei motivi per cui pensavo di imparare qualcosina di SSE e compari, anche se anche i compilatori ci stanno arrivando (ogni tanto vedo del codice generato da gcc recenti con vettorizzazione automatica che fa paura... certo, fino a qualche tempo fa ogni tanto faceva anche delle cagate apocalittiche
Infatti ci sono vere e proprie strategie per sfruttare la potenza computazionale messa a disposizione (e.g. Data-Oriented Design), aiutando dunque compilatore e processore.
Alle SSE ho dato anche io uno sguardo: alla fine non c'è nulla di complicato, se non fosse per la nomenclatura. Poi essendo il binding in C, ogni operazione ha una sua funzione che quindi rende meno naturale l'interazione (ed in fatti pensavo a sviluppare delle classi value-like per i vari tipi, ma serve comunque una certa preparazione). Altra cosa articolata potresti vederla quando devi ristrutturare il codice (cicli fondamentalmente) per poterne fare uso, tanto che i vectorizer scappano se trovano una certa forma di un ciclo.
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.
• Un plauso a Grisha Perelman, raro esempio di genuino anticonformismo umano e scientifico.
Permessi di invio
Rispondi quotando