Plus simple a utiliser..
Peut-être mais à titre personnel (et à mon grand regret) après avoir essayé de suivre des tutoriels sur Idris, ça me reste toujours hors de portée(1)!
Donc attention à ne pas sur-vendre non plus: programmer avec des preuve formelle ça reste beaucoup plus compliqué que programmer 'normalement'..
Après ce n'est pas une critique d'Idris ou des preuves formelles.
1: ou plus exactement quand je vois les efforts nécessaire rien que pour prouver des trucs simple, je n'en vois pas l'intérêt: je ne suis pas employé par Airbus..
[^] # Re: Idris
Posté par reno . En réponse à la dépêche Sortie de Coq 8.5 bêta, un assistant de preuve formelle. Évalué à 5.
Plus simple a utiliser..
Peut-être mais à titre personnel (et à mon grand regret) après avoir essayé de suivre des tutoriels sur Idris, ça me reste toujours hors de portée(1)!
Donc attention à ne pas sur-vendre non plus: programmer avec des preuve formelle ça reste beaucoup plus compliqué que programmer 'normalement'..
Après ce n'est pas une critique d'Idris ou des preuves formelles.
1: ou plus exactement quand je vois les efforts nécessaire rien que pour prouver des trucs simple, je n'en vois pas l'intérêt: je ne suis pas employé par Airbus..