Idées & Perspectives

Explorer le développement AI-first, les garde-fous de code et l'architecture de la jetabilité.

model-checkingllmrustformal-proofs

Les LLMs peuvent générer du code Rust. Les preuves formelles sont un problème entièrement différent.

Les grands modèles de langage écrivent du Rust étonnamment bon, mais quand vous leur demandez une preuve formelle, ils hallucinent des invariants et inventent une syntaxe qu'aucun vérificateur n'accepte. Voici ce qu'ils font réellement bien, où ils échouent et comment les utiliser malgré tout.

Les LLMs peuvent écrire du Rust qui compile et même passe . Ce qu'ils ne peuvent pas faire de manière fiable, c'est écrire une preuve formelle que le code est…
model-checkingtemporal-logicformal-methodsverification

Vous pouvez vérifier du code par model checking sans apprendre la temporal logic

Les bounded model checkers comme Kani et les relational model finders comme Alloy permettent de vérifier des propriétés avec des assertions et des contraintes ordinaires. Vous renoncez aux preuves de liveness pour une courbe d'apprentissage mesurée en heures.

Vous n'avez pas besoin d'apprendre la logique temporelle linéaire pour utiliser un model checker. Des outils comme Kani, CBMC et Alloy vous permettent de…
model-checkingrustverificationformal-methods

Vous pouvez prouver votre code Rust correct sans écrire une seule preuve, mais l'espace d'états est la facture

Des outils de model checking comme Kani permettent de vérifier des propriétés Rust avec des assertions au lieu de preuves formelles. Le hic, c'est ce qui se passe quand vos boucles n'ont pas de petites bornes.

Vous pouvez prouver votre code Rust correct sans écrire une seule preuve. L'outil qui le fait s'appelle un model checker, et pour Rust le plus pratique en ce…
model-checkingdistributed-systemstlaplusprotocol-design

Vous ne pouvez pas unit tester un protocole distribué, mais vous pouvez le model checker

Les bugs distribués sont coûteux à corriger après déploiement. Le model checking vous permet de les trouver avant d'écrire une seule ligne de code d'implémentation. Voici comment faire avec TLA+.

Vous ne pouvez pas unit tester un protocole distribué. Un unit test exécute un processus sur une machine dans un ordre. Votre protocole exécute dix processus…
dsls-bounded-contextinfrastructureconfig-managementdevops

Copier des fichiers `.env` d'un environnement à l'autre n'est pas une stratégie de configuration

Comment les équipes infrastructure gèrent la configuration entre dev, staging et production à l'aide de DSLs par contexte qui rendent les différences d'environnement explicites et type-safe.

Ton environnement de staging fonctionne. Ton environnement de production ne fonctionne pas. Le diff entre leurs fichiers fait 400 lignes, et la moitié de ces…
dsls-bounded-contextllmconstrained-generationgrammar

Grammar-constrained decoding : forcer les LLMs à produire une syntaxe valide à chaque token

Les LLMs hallucinent la syntaxe parce qu'ils samplent les tokens de manière probabiliste. Le grammar-constrained decoding filtre le vocabulaire à chaque étape pour n'émettre que des tokens préservant la validité syntaxique.

Demandez à un LLM de générer un objet JSON et il finira par émettre une virgule finale, un saut de ligne non échappé à l'intérieur d'une string, ou un bare…
dsls-bounded-contextdesign-systemsllmthemes

Traduire de l'anglais vers un thème est facile. Le rendre déterministe est le vrai problème.

Vous pouvez générer des design tokens à partir de descriptions en anglais simple, mais seulement si vous traitez la description comme un DSL à contexte borné avec un contrat de schema et des snapshot tests.

Oui, vous pouvez décrire un thème en anglais et obtenir un design system fonctionnel. L'astuce est que la description en anglais n'est pas un prompt. C'est un…
dsls-bounded-contextdslparser-combinatorstypescript

Oubliez le fichier de grammaire : écrivez votre parser DSL en TypeScript pur

Les générateurs de parsers sont surdimensionnés pour la plupart des DSLs à contexte borné. Les combinateurs de parsers vous permettent de construire un parser fonctionnel dans le même langage que votre application, sans code généré ni étape de build.

Si vous avez déjà ouvert un fichier de grammaire Yacc et vous êtes demandé pourquoi construire un langage nécessite d'apprendre un deuxième langage, vous…
dsls-bounded-contextconfig-validationtypescriptschemas

Les erreurs de configuration à l'exécution sont des échecs en production que vous avez choisi de tolérer

Comment attraper les erreurs de configuration avant que votre application ne commence à servir du trafic, en utilisant la validation de schémas et les vérifications au moment du build.

Votre application lance une trois heures après le début du vendredi soir. La stack trace pointe vers une propriété profondément imbriquée sur un objet de…