Si je ne me trompe ce ne sont pas les types qui calment, mais la preuve.
Après le non merci, c'est rapide comme jugement. Parfois tu veux vraiment prouver que ton code fait ce que tu lui as demandé. Et oui ça a un coût.
Ce qui est intéressant dans SPARK (en tout cas le 2014) c'est que tu peux alterner en disant que telle portion est uniquement couverte par des tests unitaires, telle portion est prouvée. Justement dans le but de réduire le coût total.
Mais ce que je trouve intéressant c'est que justement, même pour un cas hyper trivial comme chercher un élément dans une liste on se rend compte que ce n'est pas trivial au final. Rien que la valeur de retour lorsqu'on ne trouve pas d'élément est un vrai problème.
[^] # Re: Types a quel prix?
Posté par CrEv (site web personnel) . En réponse au journal De tout, de rien, des bookmarks, du bla bla. Évalué à 5.
Si je ne me trompe ce ne sont pas les types qui calment, mais la preuve.
Après le non merci, c'est rapide comme jugement. Parfois tu veux vraiment prouver que ton code fait ce que tu lui as demandé. Et oui ça a un coût.
Ce qui est intéressant dans SPARK (en tout cas le 2014) c'est que tu peux alterner en disant que telle portion est uniquement couverte par des tests unitaires, telle portion est prouvée. Justement dans le but de réduire le coût total.
Mais ce que je trouve intéressant c'est que justement, même pour un cas hyper trivial comme chercher un élément dans une liste on se rend compte que ce n'est pas trivial au final. Rien que la valeur de retour lorsqu'on ne trouve pas d'élément est un vrai problème.