컴퓨터 과학의 세계에는 프로그래밍 언리가 얼마나 유연할 수 있는지와 얼마나 안전하게 사용할 수 있는지 사이의 끊임 없는 긴장이 존재합니다. 프로그래머들은 마치 상황에 따라 도구를 바꾸는 스위스 아미 나이프처럼, 함수가 실행 중에 그 동작을 변경할 수 있는 복잡하고 동적인 시스템을 구축할 수 있는 언어를 원합니다. 그러나 이러한 유연성은 종종 대가를 치르게 합니다. 즉, 프로그램이 실제로 실행될 때 어떻게 작동할지 예측하는 것이 매우 어려워집니다. 프로그램이 작업을 마칠 것인가, 아니면 무한 루프에 빠질 것인가? 프로그램이 충돌할 것인가, 아니면 올바른 결과를 낼 것인가? 수십 년 동안 연구자들은 코드가 실행되기 전에 논리적 규칙을 따르는지 확인하여 안전망 역할을 하는 타입 시스템(type systems)이라는 체계를 개발해 왔습니다. 이 중 교차 타이핑(intersection typing)으로 알려진 특정 접근 방식은 프로그램의 동작을 분석하는 데 강력한 힘을 발휘해 왔지만, 개발자가 예상치 못한 이벤트를 가로채고 관리할 수 있게 해주는 현대적인 프로그래밍 기능인 '이펙트(effects)'에 적용될 때는 역사적으로 어려움을 겪어 왔습니다.

이 논문은 이러한 이벤트를 처리하는 현대적인 스타일의 프로그래밍을 위해, 특히 이러한 이벤트에 특화된 새로운 사고방식을 소개합니다. 연구자들인 스테파노 카토지(Stefano Catozi), 우고 달라고(Ugo Dal Lago), 타로 세키야마(Taro Sekiyama)는 프로그램이 계산하는 것뿐만 아니라, 프로그램이 주변 세계와 정확히 어떻게 상호작용하는지를 추적할 수 있는 새로운 시스템을 만들어냈습니다. 그들은 프로그램이 트리거하는 이벤트의 순서를 계산의 핵심 정체성으로 취급함으로써, 구조가 잘 잡혀 있다면 프로그램이 작업을 완수할 것임을 보장할 수 있다는 것을 발견했습니다. 나아가, 이 복잡한 시스템을 단순화함으로써 안전할 뿐만 아니라 수학적으로 예측 가능하며, 컴퓨터가 프로그램이 특정 목표에 도달할지 여부를 자동으로 검증할 수 있는 버전을 만들 수 있다는 것을 발견했습니다. 이 연구는 왜 특정 고급 프로그래밍 기능들이 자동 검증을 불가능하게 만드는지에 대한 오랜 수수께끼를 해결하며, 더 신뢰할 수 있는 소프트웨어를 구축하기 위한 명확한 길을 제시합니다.

문제를 이해하려면 먼저 현대적 프로그램이 "이펙트(effects)"를 어떻게 처리하는지를 먼저 살펴보아야 합니다. 전통적인 컴퓨팅에서 프로그램은 종종 입력을 받아 출력을 생성하는 닫힌 상자로 간주됩니다. 하지만 실제로는 프로그램이 파일을 읽거나, 사용자의 클릭을 기다리거나, 무작위 선택을 하는 등의 일을 수행해야 할 때가 많습니다. 이것들을 대수적 이펙트(algebraic effects)라고 부릅니다. 오래된 시스템에서 이러한 이펙트가 어떻게 동작하는지에 대한 규칙은 언어 내에 하드코딩되어 있었습니다. 최신 시스템에서는 프로그래머에게 자신만의 규칙을 정의할 수 있는 권한이 주어집니다. 그들은 이펙트를 가로채서 무엇을 할지 결정하고 프로그램을 계속 진행시키는 "핸들러(handler)"를 작성할 수 있습니다. 이는 매우 강력하여, 실행 취소(undo), 다양한 결과 시뮬레이션, 또는 복잡한 데이터 흐름 관리와 같은 기능을 가능하게 합니다. 그러나 이 권한에는 숨겨진 위험이 따릅니다. 핸들러가 프로그램의 흐름을 매우 다양한 방식으로 변경할 수 있기 때문에, 표준 수학적 도구를 사용하여 프로그램이 영원히 실행되는지 혹은 원하는 상태에 도달하는지를 증명하는 것이 거의 불가능해지기 때문입니다. 이전 연구들은 이러한 고급 시스템의 경우, 프로그램이 특정 결과에 도달할 수 있는지 체크하는 문제가 결정 불가능(undecidable)하다는 것, 즉 모든 가능한 사례에 대해 이를 해결할 수 있는 컴퓨터 알고리즘이 존재할 수 없음을 보여주었습니다.

이 논문의 저자들은 이를 바꾸기 위해 노력했습니다. 그들은 HEBI라고 부르는 새로운 타입 시스템을 개발하는 것으로 시작했습니다. 간단히 말해, 타입 시스템은 코드의 각 부분에 레이블을 부여하여 해당 코드가 무엇을 할 수 있는지 설명하는 규칙의 집합입니다. 여기서의 혁신은 그들의 레이블이 "행동적(behavioral)"이라는 점입니다. 단순히 "이 함수는 숫자를 입력받아 숫자를 반환한다"라고 말하는 대신, 그들의 시스템은 계산의 전체 이야기를 기술합니다. 그것은 이벤트가 발생하는 순서, 전달되는 값, 그리고 프로그램의 미래가 해당 이펙트의 결과에 어떻게 의존하는지를 기록합니다. 예를 들어, 사용자에게 선택을 요청하고 그 선택에 따라 두 가지 다른 행동 중 하나를 수행하는 프로그램을 상상해 보십시오. 새로운 시스템은 단순히 선택이 이루어졌다는 점만을 기록하는 것이 아니라, 프로그램이 취할 수 있는 모든 경로의 전체 트리를 그려냅니다. 이렇게 함으로써, 그들은 중단과 재개를 어떻게 처리하는지를 포함하여 프로그램의 정확한 동작을 포착할 수 있을 만큼 정밀한 시스템을 만들었습니다.

이 논문의 첫 번째 주요 발견은 이 새로운 시스템이 믿을 수 없을 정도로 정확하다는 것입니다. 연구자들은 만약 어떤 프로그램에 그들의 시스템 내에서 레이블을 부여할 수 있다면, 그 프로그램은 작업을 완수할 것이라는 점을 증명했습니다. 반대로, 프로그램이 작업을 완수하는 것이 보장된다면, 그 프로그램은 항상 그들의 시스템 내에서 레이블을 가질 수 있습니다. 이는 컴퓨터 과학에서 '종료 특성 규정(characterizing termination)'이라고 알려진 드물고 강력한 속성입니다. 이는 시스템이 영원히 실행되는 프로그램과 멈추는 프로그램을 완벽하게 구별한다는 것을 의미합니다. 그들은 고전적인 수학적 기법을 자신들의 새로운 행동적 레이블에 맞게 조정하여, 시스템이 핸들러와 그 핸들러가 관리하는 이펙트 사이의 복잡한 상호작용을 처리할 수 있을 만큼 견고하다는 것을 보여줌으로써 이를 달성했습니다. 이는 이전 시스템에서 발생한 결정 불가능성이 프로그래밍 스타일 자체의 내재적 결함이 아니라, 그것을 분석하는 도구의 한계였음을 입증합니다.

하지만 완벽하게 정확한 시스템은 종로 자동화하여 사용하기에는 너무 복잡한 경우가 많습니다. 연구자들은 HEBI가 모든 종료되는 프로그램을 기술할 수는 있지만, 생성될 수 있는 레이블의 수가 너무 많아 컴퓨터가 합리적인 시간 내에 모두 체크하는 것이 불가능하다는 것을 알고 있었습니다. 이는 그들의 두 번째, 어쩌면 더 실용적인 발견으로 이어졌습니다. 그들은 다음과 같이 질문했습니다. "이 강력한 시스템을 가져와서, 체크하기 쉽게 만들기 위해 일부 유연성을 제거하여 단순화한다면 어떻게 될까?" 그들은 HEB라고 불리는 더 단순한 버전을 만들었습니다. 이 버전에서도 시스템은 이벤트의 순서와 핸들러의 동작을 추적하지만, 프로그램이 분기(branch)하는 방식을 제한합니다. 즉, 프로그램이 더 선형적인 경로를 따르도록 강제하여, 가능한 변형의 수가 유한하게 유지되도록 합니다.

이러한 단순화의 결과는 돌파구였습니다. 연구자들은 이 더 단순한 시스템에 대해서는 프로그램이 특정 결과에 도달할 수 있는지 여부를 확인하는 문제가 결정 가능하다(decidable)는 것을 증명했습니다. 이는 이제 컴퓨터가 이 스타일로 작성된 프로그램이 원하는 상태에 도달할지 여부를 자동으로 검증할 수 있음을 의미합니다. 이는 유사한 시스템에 대해 그러한 검증이 불가능하다고 알려졌던 이전의 상황으로부터의 중대한 변화입니다. 성공의 핵심은 복잡한 행동적 성격의 원래 시스템을 더 단순한 시스템을 위한 "정제(refinement)"로 사용할 수 있다는 점을 깨달은 데 있었습니다. 그들은 HEB의 단순한 규칙에 부합하는 모든 프로그램이 복잡한 HEBI 시스템의 특정하고 유한한 기술 세트로 매핑될 수 있음을 보여주었습니다. 이 집합은 유한하기 때문에, 컴퓨터는 답을 찾기 위해 이를 철저히 탐색할 수 있습니다.

이 연구는 또한 기존 시스템들이 왜 실패했는지에 대해서도 빛을 비춥니다. 연구자들은 이전의 접근 방식에서 나타난 결정 불가능성이 프로그램의 동작을 정제하는 방법이 무한한 수만큼 허용되었기 때문임을 입명했습니다. 이전 시스템에서는 단일 타입이 무한히 많은 서로 다른 변형으로 확장될 수 있었기에, 이를 모두 체크하는 것이 불가능했습니다. 반면, 그들의 새로운 시스템은 풍부한 행동적 세부 사항을 보존하면서도 이러한 변형을 유한하게 유지하는 구조를 부과합니다. 이는 더 단순한 프로그래밍 모델과 더 강력한 최신 모델 사이의 복잡성 급증에 대한 명확한 설명을 제공하며, 그 복잡성을 다스릴 수 있는 구체적인 방법을 제시합니다.

이 연구의 영향은 단지 이론에만 국한되지 않습니다. 이는 우리가 매우 유연하면서도 엄격하게 검증 가능한 프로그래밍 언어를 구축할 수 있음을 시사합니다. 이벤트의 순서를 포착하는 행동적 타입을 사용함으로써, 개발자는 코드의 안전성을 증명하는 능력을 희생하지 않으면서도 복잡한 현실 세계의 상호작용을 처리하는 코드를 작성할 수 있습니다. 연구자들은 단순히 새로운 아이디어를 제안한 것이 아니라, 그들의 시스템이 실행 중인 코드의 안전성을 보존하고 도달 가능성 속성을 자동으로 검증하는 데 사용될 수 있음을 보여주는 완전한 수학적 증명을 제공했습니다. 이는 의료 기기, 금융 시스템, 또는 자율 주행 차량과 같이 실패가 용납되지 않는 시스템을 위한 더 신뢰할 수 있는 소프트웨어를 작성하는 데 도움이 될 미래의 도구들을 향한 문을 열어줍니다.

결국, 이 논문은 균형을 찾는 것에 관한 것입니다. 프로그램에서 복잡하고 동적인 이벤트를 처리하는 능력이 예측 가능성을 희생하며 오지 않는다는 것을 보여줍니다. 계산의 최종 결과보다는 계산의 이야기 자체에 집중함으로써 프로그램의 동작을 바라보는 방식을 바꿈으로써, 연구자들은 현대 프로그래밍의 유연성과 형식 검증의 안전성 사이의 가교를 만들었습니다. 그들은 적절한 도구가 있다면 가장 복잡한 소프트웨어 동작조차 이해하고 통제할 수 있으며, 우리의 디지털 시스템이 더욱 복잡해지더라도 신뢰성을 유지할 수 있도록 보장할 수 있음을 보여주었습니다. 이 연구는 컴퓨터 과학의 실질적인 문제를 해결하는 데 있어 세심한 수학적 분석이 가진 힘을 보여주는 증거이며, 차세대 프로그래밍 언어를 위한 새로운 토대를 제공합니다.