Limites, force de l'évidence et évaluation globale

论文版本948a07b (main)

Les garanties formelles de l'article sont élégantes, mais elles reposent sur des préconditions strictes et la force de l'évidence est limitée. Considérer les deux objectivement est nécessaire pour juger correctement si DeepSeek Harness est déjà « entièrement vérifié en production ».

Préconditions strictes

[Conclusion originale de l'article §3.1.3, §3.3.2, §4.4, §6.1] Les garanties de l'article reposent sur les préconditions suivantes ; les violer invalide les conclusions :

1. Les inverses doivent être correctement fournis par les développeurs : ctx.effect ne vérifie pas la condition witness g(δ) = γ ; un inverse erroné entraîne un échec de récupération ou une pollution d'état (§5.1.1).
2. Seuls les effets de bord gérés via le Context peuvent être suivis : modifier directement des variables globales, des fichiers, des bases de données ou des systèmes externes contourne les garanties.
3. Les emissions externes ne peuvent généralement pas être véritablement réverties : requêtes réseau, messages, emails, paiements, une fois émis, franchissent la frontière du système (§6.1). Les opérations externes ne peuvent utiliser que withholding ou compensation — cette dernière est une relation d'équivalence plus grossière, et les preuves de commutation de l'article doivent être réétablies.
4. Les plugins non fiables ont toujours besoin d'un sandbox processus/conteneur/WASM : le contrôle d'accès au niveau Context ne peut pas remplacer l'isolation de sécurité (§6.3).
5. Le graphe des dépendances doit être acyclique : ≺ acyclique est une hypothèse de Progress et Confluence (§4.4.4, §4.4.5) ; l'auto-dépendance (n ≺ n) entraîne un deadlock.
6. Les composants et itérations doivent être en nombre fini : len(e_n) ≤ K et des noms de fibers finis sont des hypothèses de Progress (§4.4.4) ; l'auto-enregistrement non borné casse la terminaison.
7. Les effects doivent être mutuellement indépendants ou commutatifs : Recovery Exactness exige pairwise independence (§4.4.2) ; les effects médiés par coeffect satisfont la commutativité via les clés (Thm 42) ; les clés non commutatives (p. ex. chaînes ordonnées) nécessitent un ordonnancement par coeffect.
8. Component total on provision : Confluence exige que chaque component installe effectivement toutes les keys qu'il déclare (§4.4.5 Def 69).
9. Confluence exclut les scénarios de failure : les fibers échoués sont une véritable source de divergence.
10. La compatibilité de version et structurelle des clés de dépendance reste un problème ouvert : §6.6 note que le nominal linking ne fournit pas de vérification de compatibilité versioned ou structural ; l'interface drift et la key collision n'ont pas de solution indépendante du langage.

Force de l'évidence

[Conclusion originale de l'article §5.3] Évaluation objective :

• Koishi a 4000+ plugins communautaires et est un cas de production important ; l'article se positionne comme « un résultat d'existence et d'adoption plutôt que quantitatif » (preuve d'existence et d'adoption, pas une expérience contrôlée quantitative).
• L'article reconnaît : l'évidence provient d'un seul écosystème et d'un seul langage hôte ; la contribution du paradigme ne peut être séparée de la contribution de l'implémentation TypeScript ou du domaine Koishi ; c'est observationnel et non une comparaison contrôlée ; il ne mesure pas le overhead d'abstraction ni l'impact sur la productivité des développeurs.
• L'article décrit Cordis v4, tandis que Koishi utilise Cordis v3 en production ; la note de bas de page §5.3 de l'article est explicite : « the core compositional model is shared across both versions » — le modèle central est partagé, mais la sémantique d'effect/coeffect et le loader de v4 sont repensés. L'évidence de production des 4000+ plugins de Koishi correspond à v3, pas au v4 décrit dans l'article.
• DeepSeek Harness est encore en Developer Preview ; la déclaration officielle : « core plugins and APIs are expected to continue evolving ».
• La conclusion §8 de l'article liste explicitement « self-evolving Agent Harness » comme direction de future validation : « Applying Cordis in such a setting would validate the temporal guarantees... » — c.-à-d. que l'article lui-même ne prétend pas avoir été validé dans le scénario de l'Agent auto-évolutif.
• Le paquet cœur de Cordis est actuellement en 4.0.0-rc.x, et 4.0.0 n'a pas encore été officiellement publié.

[Évaluation personnelle] N'équipez pas la preuve du modèle théorique avec le produit DeepSeek Harness déjà entièrement vérifié en production — le premier est un théorème mathématique valable sous plusieurs hypothèses, le second est un système d'ingénierie en Developer Preview. La relation est « DSH est construit sur Cordis, et Cordis implémente le modèle de l'article », pas « DSH a déjà prouvé toutes les conclusions de l'article ».

Évaluation globale

Innovation majeure

[Évaluation personnelle] L'innovation systémique majeure de l'article est d'élever la paire de concepts classiques de théorie des types statiques effect et coeffect à des mécanismes à l'exécution, unifiés dans un seul type de context. Ce n'est pas une simple combinaison — effect/coeffect existe depuis longtemps en théorie des langages de programmation (Moggi 1991, Petricek 2013, Gaboardi 2016), mais comme outils d'analyse statique à la compilation. Cordis les réifie en objets de première classe à l'exécution, élevant « les composants peuvent être chargés, déchargés, remplacés » de la pratique d'ingénierie à un calcul formel avec des garanties métathéoriques. Le théorème de Confluence est le point culminant de cette innovation : l'histoire dynamique ne laisse pas de trace, équivalente à l'assemblage statique.

Ce qui est une recombinaison d'idées préexistantes

[Évaluation personnelle] Beaucoup de composants de l'article sont des concepts préexistants :

• Effect + Inverse : dagger arrows (Heunen et al.), le pattern Command (undo/redo), Saga (compensating action), STM (read/write log + abort) ;
• Coeffect + Reactivity : OSGi Declarative Services, iPOJO Gravity, FRP/Signals ;
• DI + Lifecycle : Spring, Angular hierarchical injectors, Vue provide/inject ;
• HMR : webpack, Vite (mais nécessite des boundaries écrits à la main) ;
• RAII / Linear types : lier release au scope lexical ;
• Capability-based security : la déclaration ctx.inject est une demande de capability ;
• React useEffect : appareillement effect + cleanup, mais restreint ; React Fiber : une unité de reconciliation.

L'innovation de Cordis n'est dans aucun composant individuel, mais dans leur assemblage en un tout intégré : « chaque effect atomique porte un inverse + chaque coeffect est automatiquement réactif + un context unifié + une machine à états complète de cycle de vie + une métathéorie formelle ».

La valeur systémique que Cordis ajoute vraiment

[Évaluation personnelle]

1. Dérivation structurée des inverses : les développeurs n'écrivent des inverses que pour les effects atomiques, et les inverses composites sont dérivés automatiquement via ⋄ ; React useEffect ne peut y parvenir en raison des restrictions des hooks.
2. Garantie formelle de l'ordre de déchargement Provider/Consumer : l'état intermédiaire Unloading + le guard ¬ relied élèvent « attendre que les consumers soient déchargés avant de retirer le provider » d'une convention à une imposition à l'exécution ; le callback de deactivation synchrone d'OSGi n'y parvient pas.
3. Une machine à états inertielle pour async + changements de dépendances : les deux branches de L-Divert (abort, ou land + unload) + la règle d'Inertia garantissent que les changements de dépendances pendant le chargement asynchrone ne laissent pas d'états à moitié construits ; des systèmes comme iPOJO n'ont pas un tel mécanisme.
4. Confluence : la garantie que l'histoire dynamique ne laisse pas de trace est quelque chose que les autres frameworks DI/HMR ne fournissent pas.

Projets adaptés

[Évaluation personnelle]

• Adapté : les frameworks d'application avec un écosystème riche en plugins (p. ex. Koishi, IDEs de type VSCode, agent harnesses) ; les systèmes de développement nécessitant le HMR ; les systèmes multi-tenant / multi-workspace ; les systèmes auto-évolutifs dont la topologie de dépendances des composants change fréquemment.
• Non adapté : Agents simples de type requête-réponse (pas de plugins, pas de remplacement à chaud, pas de sous-Agents) — introduire ctx.effect/fiber/inertia ici est de la sur-ingénierie ; calcul de fonctions purement sans état ; systèmes fortement dépendants des emissions externes qui ne peuvent ni withholding ni compensation (trading en temps réel, envoi de messagerie instantanée).

Ce qui manque encore pour des « Agents auto-évolutifs sûrs »

[Évaluation personnelle] La conclusion §8 de l'article liste self-evolving agent harness comme direction de future validation, ce qui signifie que l'article lui-même ne prétend pas l'avoir résolu. Il manque encore :

1. Sandbox pour code non fiable : §6.3 est explicite que le contrôle d'accès au niveau du langage est insuffisant contre les composants malveillants ; l'isolation au niveau OS/WASM/processus est nécessaire — l'article ne la fournit pas.
2. Rollback des emissions externes : requêtes réseau, paiements, emails ne peuvent pas être véritablement révertis, seulement withhold ou compenser ; un Agent auto-évolutif se modifie fréquemment, et chaque modification peut déclencher une chaîne d'emissions nécessitant un design de compensation.
3. Interface drift et key collision : §6.6 souligne que la compatibilité de version et structurelle des clés de dépendance est un problème ouvert ; les composants générés par un Agent auto-évolutif peuvent ne pas suivre les contrats d'interface existants.
4. Overhead de performance et mémoire : l'article ne donne pas de données quantitatives ; une closure/iterator par effect, un accumulator + committed view par fiber — le overhead mémoire et CPU n'est pas mesuré.
5. Confluence sous modes de failure : le théorème de Confluence exclut explicitement le failure ; dans les Agents auto-évolutifs, les échecs sont la norme (le code généré peut contenir des syntax errors), et les fibers échoués n'affectent pas l'état mais laissent une divergence de « même configuration, états différents ».
6. Support multilangage : §6.4 discute des exigences d'indépendance du langage, mais l'implémentation de Cordis est actuellement en TypeScript ; comment unifier sous le context de Cordis des outils dans plusieurs langages générés par un Agent auto-évolutif n'est pas clair.

Ordre de lecture recommandé

1. §1 Introduction + §1.2 Motivating Examples : comprendre le problème — pourquoi le système de plugins de VSCode est insuffisant, pourquoi Agent Harness a besoin de composition dynamique, pourquoi les substituts à granularité grossière ne suffisent pas.
2. §2 Preliminaries : un rappel rapide de la théorie classique effect/coeffect. Les lecteurs peu familiers avec la théorie des langages de programmation peuvent sauter les formules mathématiques et seulement retenir « effect = modifier l'environnement, coeffect = dépendre de l'environnement ».
3. §3.1 Revertible Effects : se concentrer sur Def 8 (witnessed effect function), Thm 7 (recovery), Thm 16 (LIFO). Comprendre la correspondance mathématique de ctx.effect.
4. §3.2 Reactive Coeffects : se concentrer sur Def 26 (activating/deactivating/neutral) et la synergie de set comme effect (fin de §3.2.1).
5. §3.3 The Context Paradigm : comprendre la structure récursive de Γ∞ (Def 32) et comment l'observational equivalence (§3.3.2) « achète » l'indépendance.
6. §4.1-4.2 Components and Base Calculus : comprendre fiber, committed view, target view, les cinq règles de base.
7. §4.3 Transitions in Progress : se concentrer sur §4.3.1 Withdrawal (L-Leave + guard) et §4.3.2 Iteration (effect iterator et L-Divert).
8. §4.4 Metatheory : les énoncés des 6 théorèmes (les preuves peuvent être sautées). Se concentrer sur le sens ingénierie de Confluence (Thm 73).
9. §5 Implementation : croiser Table 2 pour voir ctx.effect, ctx.set, Algorithm 4 (ctx.use), Algorithm 5 (refresh/reload/unload).
10. §5.3 Koishi Case Study + §6 Discussion + §7 Related Work : comprendre la force de l'évidence de production, la frontière du système (§6.1 acquisition vs emission), la relation avec OSGi/React/STM/AOP.
11. §8 Conclusion : clarifier que la direction de future validation est self-evolving agent harness.

Notes connexes

• Autres chapitres de ce site : Contexte et problème · Effects · Coeffects · Cycle de vie · Théorèmes · DeepSeek Harness
• Article original : cordiverse/paper
• Analyse de l'architecture DeepSeek Harness (site sœur) : dsh.arch.tools-ai.org