EFCH Lang — Lenguaje y Cadena de Herramientas
EFCH Lang es un lenguaje de programación y cadena de herramientas experimental que explora contratos explícitos y comportamiento verificable, inicialmente dentro de dominios de programas acotados.
LÍNEAS DE VERSIÓN // ARQUITECTURA
Líneas de versión: 0.1.x (Alpha) frente a 0.2 (En desarrollo)
0.1.x — Línea Alpha de Mantenimiento y Herramientas
Alpha actual (0.1.0a1 / 0.1.x)Enfocada en decodificación binaria acotada, operaciones sobre vectores de bits, esquemas canónicos de evidencia e integración con editores y SDKs.
- Modelo dual de archivos: especificaciones formales en expresiones S (.efch) junto con módulos de implementación (.efl)
- Esquema JSON canónico de evidencia (efch-evidencia/1.0) emitido por efch export check y efch export lang
- SDK en TypeScript (efch-lang-sdk-ts) y SDK para .NET 8 (EfchLang.Sdk) para integración en pruebas y CI
- Servidor Language Server Protocol v3.17 (efch-lang-lsp) y extensión para VS Code (v0.1.2)
0.2 — Línea de Evolución Semántica
En desarrollo · No publicadaTrabajo exploratorio en desarrollo con nuevas capacidades semánticas para abordar las restricciones del dominio 0.1.
- En fase de diseño e investigación interna
- No publicada como release ni disponible aún para instalación pública
Capacidades comprobadas en 0.1.x (en dominios acotados)
- +01Comprobación de especificaciones (efch check): descarga obligaciones de tipos y buena definición en especificaciones .efch mediante Z3.
- +02Verificación de equivalencia y propiedades (efch verify): demuestra o refuta con contraejemplos concretos si una candidata .efl/.efch cumple su especificación formal.
- +03Generación de código C (efch build): emite implementaciones en C a partir de candidatas verificadas para compilación con gcc -O2 y pruebas diferenciales.
- +04Diagnósticos en editor y CI: expone contraejemplos SMT concretos y navegación entre especificación e implementación mediante LSP v3.17.
Limitaciones actuales y restricciones del dominio
- !01Modelo de ejecución estrictamente acotado: sin bucles no acotados, recursión, memoria dinámica ni efectos secundarios.
- !02Límite de tamaño de entrada: las entradas bytes están restringidas a un máximo de 64 bytes en el núcleo 0.1.0a1.
- !03Backend en C no verificado formalmente: el traductor del núcleo EFCH a C se valida con pruebas diferenciales.
- !04Tiempos límite en SMT: propiedades aritméticas complejas sobre vectores de bits pueden devolver 'desconocido' al superar el presupuesto del solucionador.
- !05Visibilidad de repositorios: mientras el núcleo EFCH Lang 0.1 y sus pruebas están publicados en efch-artifacts-p2-lang-binary-decoding, los repositorios individuales de SDK/LSP/VS Code en @venture-synaptic permanecen privados hasta su aprobación de apertura.
REPRODUCCIÓN DE COMANDOS
Comandos de verificación comprobados (Paquete Público P2)
Los siguientes comandos están verificados sobre el repositorio público venture-synaptic/efch-artifacts-p2-lang-binary-decoding (requiere Python >= 3.10 y gcc en entorno Linux/POSIX):
Componentes del ecosistema EFCH Lang
Archivo público con la implementación del núcleo EFCH 0.1 y EFCH Lang, 178 pruebas unitarias y scripts reproducibles para EXP-004 a EXP-015.
SDK oficial en TypeScript para interactuar con el compilador, verificador formal y diagnósticos CLI de EFCH 0.1.x.
SDK en .NET 8 (EfchLang.Sdk) basado en el esquema canónico efch-evidencia/1.0 para integración en pruebas C# / xUnit.
Servidor Language Server Protocol (v3.17) para archivos .efl y especificaciones .efch construido sobre efch-lang-sdk-ts.
Extensión de VS Code para resaltado sintáctico, comandos de verificación formal e integración LSP en archivos .efl y .efch.