A l'origine, ce n'était qu'un lien mais finalement, cela méritait un journal sur Spark.

Avant de vous filer le lien sur le portage, on va commencer par un petit exemple rapide de ce que peut faire Spark.

Mais c'est quoi Spark ?

Spark est, aujourd'hui, un sous-ensemble d'Ada restreignant les capacités aux fonctions sécurisées et non-abmigües.

Via un ensemble d'aspects, une sorte d'annotations, le compilateur gnatprove génère des conditions de vérification pour chaque sous-programme.
Ces conditions de vérification (…)