Je travaille sur la spécification Concrete v2. La première version a déjà un code fonctionnel et nous avons beaucoup appris en l'implémentant. Maintenant, j'ai ajouté de nouvelles fonctionnalités intéressantes qui proviennent de Zig, Austral, Lean/Coq. Je conçois un langage de systèmes axé sur la vérification formelle dès le départ avec des fonctionnalités intéressantes. Fonctionnalités : - noyau formalisé dans Lean 4 - types linéaires (style Austral, pas affine de Rust) - emprunt sans annotations de durée de vie - capacités pour le suivi des effets - allocateur passé comme capacité (style Zig) - pur par défaut - ! pour les fonctions impures (de Roc) Comment elles se composent : Les types linéaires sont la fondation. Chaque valeur consommée exactement une fois. Pas de fuites, pas de double libération, pas d'utilisation après libération. Sécurité mémoire sans GC. C'est plus verbeux mais plus concret et clair que les types affines. L'emprunt rend la linéarité utilisable. Référencer temporairement une valeur sans la consommer. Régions lexicales au lieu des annotations de durée de vie de Rust. Le compilateur infère ce que Rust vous oblige à écrire. Les capacités suivent les effets. Une fonction qui lit des fichiers le déclare. Une fonction qui alloue le déclare. Pas de déclaration signifie pas d'effets, garanti. grep avec(Network) trouve chaque fonction qui touche le réseau. L'allocateur comme capacité rend l'allocation visible. Le code sans with(Alloc) ne touche jamais la heap, prouvé. Vous contrôlez quel allocateur sert quel chemin de code. Allocation d'arène, de pool, de pile, tout explicite. Pur par défaut inverse le modèle habituel. Les effets nécessitent une déclaration. Le cas commun (calcul pur) n'a pas besoin d'annotation. Le noyau Lean lie le tout. Lorsque le compilateur dit que votre programme est sûr, cette affirmation est soutenue par une preuve.