Le **/* et *~*.ogg... Hihi. Ca me rappelle la première version du A~B où B pouvait être vide... et où des devs, après une longue nuit de code, avaient voulu effacer les backups emacs avec **/*~ (à savoir, à l'époque, tout récursivement sauf rien...)
Quand on arrive à démontrer que 1 est égal à 2 via un raisonnement mathématique érroné, ce n'est ni les mathématiques qu'il faut remmetre en cause, ni la fiabilité de l'opérateur égal, mais bien le raisonnement.
Le dernier aspect, celui de l'implémentabilité, est le plus drole. On peut le résumer ainsi : "Machine de Turing complète". En d'autres termes si on fait fi du temps d'éxecution et de l'occupation mémoire on peut écrire un programme en C pour tout algorithme calculable. Au final tout est implémentable. Mais il y a un hic, aucun programme au monde ne pourra jamais prendre en entrée un n'importe quel autre programme et déterminer si oui ou non celui ci va finir. Ce problème est dit 'non décidable'. Pour résumer : pour valider de façon certaine une implémentation il faut la "prouver". Le problème de la preuve est un problème complexe, sur un OS évolué, le plus simple des programmes peut se retrouver mis continuellement en attente par des jeux d'interruptions, de priorités et de blocages de ressources qui font qu'il ne se terminera jamais. Donc l'implémentation du plus simple des programmes Linux est fausse.
Un algorithme complexe et nouveau vient souvent avec sa preuve decidabilite sur un modele d'execution abstrait. Pour les systemes critiques, on peut avoir des preuves plus formelles, voir des preuves vis-a-vis du materiel sous-jacent. Ca me parait etre une condition suffisante de son implementabilite. Surtout si en plus une implementation effective est donnee (voire avec ses parties critiques prouvees formellement).
[^] # Re: zsh-lovers
Posté par Burps . En réponse à la dépêche À la (re)découverte de Zsh. Évalué à 3.
Ca avait bougé dans la ML !
[^] # Re: Il va falloir arreter les anneries très vite.
Posté par Burps . En réponse à la dépêche Lettre du président de la FSF Europe à l'EICTA au sujet des brevets logiciels. Évalué à 3.
Sauf le jour ou Russell ecrivit a Frege :)
[^] # Re: Il va falloir arreter les anneries très vite.
Posté par Burps . En réponse à la dépêche Lettre du président de la FSF Europe à l'EICTA au sujet des brevets logiciels. Évalué à 2.
Un algorithme complexe et nouveau vient souvent avec sa preuve decidabilite sur un modele d'execution abstrait. Pour les systemes critiques, on peut avoir des preuves plus formelles, voir des preuves vis-a-vis du materiel sous-jacent. Ca me parait etre une condition suffisante de son implementabilite. Surtout si en plus une implementation effective est donnee (voire avec ses parties critiques prouvees formellement).