COBOL to Kotlin via Formal Models (IR and Alloy and Golden Master)
15 days ago
- #Modernization
- #COBOL
- #Formal Methods
- COBOL remains a critical backbone for financial and administrative systems globally, handling significant portions of banking, insurance, and healthcare operations.
- Modernization of COBOL systems requires a verifiable approach, focusing on semantic reconstruction rather than simple translation to ensure functional equivalence.
- The experiment involves transforming a COBOL batch program into an intermediate representation (IR), modeling it formally, generating Kotlin code, and verifying equivalence.
- Formal methods like Alloy, TLA+, and SMT (Z3) are used to verify invariants, temporal behavior, and arithmetic/logical consistency in the modernized code.
- A Golden Master approach ensures behavioral equivalence by comparing outputs from COBOL and modern implementations using checksums.
- The repository structure includes COBOL source, IR, formal models, Kotlin code, and scripts for parsing, verification, and comparison.
- Future steps include extending the COBOL parser, enhancing formal models, and evolving the Kotlin runner into a microservice.
- LLMs can assist in modernization when guided by formal context, acting as semantic compilers within a constrained framework to ensure correctness.
- Modernization is framed as an epistemic challenge, reconstructing system truths to move beyond legacy debt with verifiable, scientific processes.