hum-lang

Hum est une ébauche de conception à un stade précoce (0.0.1 pré-alpha) pour un langage de programmation système. Son objectif déclaré est de combiner la puissance de bas niveau de style Rust/C++ avec une lisibilité proche de Python, des types statiques, des effets explicites, la sécurité mémoire par défaut et un contexte généré par le compilateur destiné à la fois aux humains et aux agents de codage. L'idée centrale est que les contrats habituellement écrits sous forme de commentaires deviennent des promesses vérifiées. Une tâche peut déclarer des sections telles que `why`, `targets`, `uses`, `changes`, `needs`, `ensures`, `protects`, `trusts`, `fails when`, `watch for`, `cost`, `allocates`, `avoids`, `tradeoffs`, `optimizes`, `tests` et `does`. Le dépôt inclut un cas de test délibérément saboté dont le `ensures: result == a + b` est violé par un corps `return a - b` ; son exécution produit un diagnostic qui met en cause l'implémentation de la tâche plutôt que l'appelant. Les mots de propriété (`borrow`, `change`, `consume`) sont également traités comme des promesses vérifiées. Les vues locales sont étroites : l'emprunt d'un champ est invalidé par une écriture ultérieure dans ce champ, et l'emprunt d'un élément de liste est invalidé par une croissance ultérieure. Une forme d'alias inscriptible (`let alias = change record.field`) écrit à travers et n'est vivante que jusqu'à sa dernière utilisation syntaxique en ligne droite. L'utilisation après déplacement est signalée avec le site de déplacement nommé. `old(...)` capture la valeur d'un paramètre à l'entrée de la tâche, de sorte qu'un échange qui n'échange jamais est détecté par son propre contrat. Le README est explicite sur les limites : les lignes `cost:`, `allocates:`, `protects:` et `trusts:` sont aujourd'hui une intention enregistrée, des faits de graphe et des obligations générées, et non des preuves appliquées. Les rapports du vérificateur émettent une liste explicite de non-revendications afin que la frontière entre ce qui est vérifié et ce qui est déclaré reste visible. Statut : un front-end de compilateur bootstrap en Rust pour le jalon 0, avec l'exécution du jalon 1 amorcée via `hum run` qui interprète les premiers cas de test du Formal Core. La première tranche native canonique est `programs/integer_sign.hum`, exécutée avec `hum run --native --allow stdout.write ... --args -7`, qui vérifie la source, valide les faits du backend et imprime via Cranelift sur les hôtes Windows et Linux pris en charge. Le README décrit cela comme une forme de programme délimitée, et non comme une compilation native générale. Le dépôt est riche en documentation : architecture, référence du langage, grammaire, schémas pour la surface syntaxique, capacités, faits de cible, rapports de preuves, obligations mathématiques, rapports de ressources, contrat/aperçu/abaissement/vérification de Core Hum, vérifications de type/effet/propriété/ressource, contrat et préparation de l'IR, entrée/sonde/contrat du backend, capacités LSP, doctor, ainsi que des enregistrements de décisions, le modèle de sécurité, la politique unsafe, l'interopérabilité et la portabilité, le modèle de sécurité mémoire, la stratégie de compilation, la stratégie de bibliothèque standard, les profils d'exécution, la stratégie de backend, la feuille de route, la gouvernance et des notes de recherche. L'outillage comprend une grammaire TextMate, un formateur prévu (`humfmt`), un plan de gestionnaire de paquets (Nectar) et des commandes CLI telles que `check`, `version`, `explain`, `diagnostics`, `capabilities`, `target-facts`, `core-contract`, `core-preview`, `core-lower`, `core-verify` et `full-type-check`, plusieurs avec sortie JSON. Le compilateur bootstrap est écrit en Rust et interdit le code unsafe par défaut, avec une frontière d'invocation JIT unsafe revue et autorisée localement, et cinq dépendances Cranelift épinglées. Cargo est le chemin actuel de compilation et d'installation, bien que le README note que Hum ne devrait pas être positionné comme « juste une crate Cargo » à long terme.