의도 기반 컴퓨팅 (Intent-Driven Computing): 통제된 자율 시스템을 위한 계산 모델

프로그래밍 언어는 프로그램이 효과 (effects)를 직접 실행한다고 가정합니다. 자율 시스템이 행동을 동적으로 생성할 때, 이러한 가정은 문제가 됩니다. 즉, 행동하기로 결정하는 것과 실제로 행동하는 것 사이에 구조적인 중재 지점이 존재하지 않습니다. 우리는 의도 기반 컴퓨팅 (intent-driven computing)을 정의합니다. 이는 프로그램이 효과를 직접 실행하는 대신 의도 (intents, 제안된 행동을 설명하는 유한한 데이터 값)를 생성하는 프로그래밍 모델입니다. 통제된 런타임 (governed runtime)은 결정 가능한 정책 언어 (decidable policy language)를 바탕으로 각 의도를 검토하고, 모든 결정을 변조 방지 원장 (tamper-evident ledger)에 기록한 다음, 그제서야 효과를 실현합니다. 이 언어는 효과로 가는 다른 대안 경로를 제공하지 않습니다. 이 모델은 프로그램의 임의적인 행동 속성을 결정하지 않습니다 (Rice의 정리에 따르면 이는 불가능합니다). 대신, 모든 효과적인 상호작용이 유한한 의도 값으로 구체화 (reified)되도록 언어를 제약함으로써, 거버넌스 (governance)의 영역을 프로그램 의미론 (program semantics)이라는 결정 불가능한 영역에서 의도 데이터 (intent data)라는 결정 가능한 영역으로 전환합니다. 이를 통해 다음과 같은 창발적 속성 (emergent properties)이 나타납니다: 구조적으로 보장되는 이벤트 소싱 (event sourcing), 의도 재생 (intent replay)을 통한 거버넌스 시뮬레이션, 구조적 감사 완전성 (structural audit completeness), 그리고 향상된 인간 이해도입니다. 우리는 이 모델을 공식적으로 명시하고, BEAM 가상 머신 (virtual machine)으로 컴파일되는 구체적인 언어로 구현하였으며, Rocq에서 주요 속성들을 검증하였습니다 (454개의 정리, 36개의 모듈, 허용된 보조정리 0개). 속성 기반 테스트 (property-based testing, 70,000개 이상의 무작위 입력, 불일치 0건)를 통해 구현이 명세와 일치함을 확인했습니다.