27-08-2013, 03:19 PM
La granularité adaptée me semble être la fonction (le grain élémentaire du langage).
Je ne pense pas qu'il serait visualisable dans son ensemble, humainement, mais cela me semble aussi utile que vouloir visualiser toute une base de donnée d'un bloc.
Si la fonction Square() est ajoutée, la preuve serait faite par l'outil automatisé (car oui, je redis: à la main, ça serait long
).
Si tu veux calculer un carré de décimaux, oui, il te faudra une autre fonction: soit une nouvelle, soit un upgrade de la fonction square(). Tu peux aussi simplement passer le typage de "int" vers "double", mais la fonction ne sera plus prouvée, et toutes celles qui l'utiliseront pourront voir apparaitre un bug.
Le langage évoluent, les patch et hotfix ne sont là qu'à cause de l'implémentation que l'on en fait (implémentation non prouvée justement). Les langages sont l'objet d'études avancées dans les labos de recherche, par les bons gros matheux bien chers et rares. Toutes les situations peuvent se résoudre par équation: l'informatique, c'est des machines de Turing, des machines d'état finis. Ca s'étudie, c'est juste long. A la main, ce serait lourd, mais si c'est la machine qui le fait, c'est tout bénef'.
D'accord, je partage l'opinion que c'est pour l'instant le meilleur ratio qualité/prix pour les systèmes courants; ça n'empêche pas que j'aimerai bien pousser et réussir à ouvrir une autre voie d'étude pour le développement :p
Je ne pense pas qu'il serait visualisable dans son ensemble, humainement, mais cela me semble aussi utile que vouloir visualiser toute une base de donnée d'un bloc.
Si la fonction Square() est ajoutée, la preuve serait faite par l'outil automatisé (car oui, je redis: à la main, ça serait long
).Si tu veux calculer un carré de décimaux, oui, il te faudra une autre fonction: soit une nouvelle, soit un upgrade de la fonction square(). Tu peux aussi simplement passer le typage de "int" vers "double", mais la fonction ne sera plus prouvée, et toutes celles qui l'utiliseront pourront voir apparaitre un bug.
Le langage évoluent, les patch et hotfix ne sont là qu'à cause de l'implémentation que l'on en fait (implémentation non prouvée justement
). Les langages sont l'objet d'études avancées dans les labos de recherche, par les bons gros matheux bien chers et rares. Toutes les situations peuvent se résoudre par équation: l'informatique, c'est des machines de Turing, des machines d'état finis. Ca s'étudie, c'est juste long. A la main, ce serait lourd, mais si c'est la machine qui le fait, c'est tout bénef'.D'accord, je partage l'opinion que c'est pour l'instant le meilleur ratio qualité/prix pour les systèmes courants; ça n'empêche pas que j'aimerai bien pousser et réussir à ouvrir une autre voie d'étude pour le développement :p