형식 기법과 프로그래밍의 미래

1 day ago 7

형식 기법은 소프트웨어가 의도한 성질을 만족하는지 증명하는 도구이며, 에이전트 코딩 확산으로 비용·효용 판단이 달라지고 있음
Jane Street은 과거 형식 기법이 일부 특수 사례를 제외하면 비용 대비 가치가 낮다고 봤지만, 이제 전담 팀을 만들고 있음
seL4는 8,700줄 C 코드 검증에 25인년이 들었고, 코드 한 줄마다 약 23줄의 증명과 반 인일 검증이 필요했음
에이전트가 생성한 코드는 출시 가능한 품질과 차이가 있으며, 검증 병목을 줄이고 에이전트에 강한 피드백을 주는 수단으로 형식 기법이 중요해짐
Jane Street은 언어를 깊게 통제할 수 있고 준비된 프로그래머 커뮤니티가 있어, OxCaml과 증명 지향 기법을 함께 발전시킬 여지가 있다고 봄

형식 기법과 프로그래밍의 미래

Jane Street은 지난 25년 동안 조직 차원에서 형식 기법에 관심이 없다고 말해 왔지만, 이제는 그 입장을 유지하지 않음
더 나은 코드와 더 신뢰할 수 있는 코드를 쓰기 위한 도구의 힘은 오래전부터 중시해 왔고, 타입 시스템은 큰 이득을 준 가벼운 형식 기법으로 여겨짐
특수 사례, 특히 하드웨어 합성을 제외하면 형식 기법은 비용이 너무 커서 대부분의 소프트웨어에 맞지 않는다고 판단해 왔음
seL4는 형식 검증된 마이크로커널이자 중요한 성취였지만, 8,700줄 C 코드 검증에 25인년이 들었음
- 코드 한 줄마다 약 23줄의 증명이 필요했고, 한 줄 검증에 약 반 인일이 필요했음
보안이 중요한 마이크로커널처럼 위험이 크고 명세가 비교적 명확한 경우에는 이런 접근이 가치 있을 수 있음
대부분의 소프트웨어에는 맞지 않았고, Jane Street의 가장 중요한 소프트웨어에도 맞지 않는다고 느껴졌음
에이전트 코딩의 등장이 판단을 바꾸었고, 형식 기법 가능성에 대한 회의가 기대감으로 전환됨
Jane Street은 형식 기법 팀을 만들고 있으며, 정교한 타입 시스템만큼 널리 유용한 소프트웨어 구축 도구로 만들기를 기대함

왜 마음이 바뀌었나

에이전트 코딩은 여러 방식으로 형식 기법의 기존 비용·효용 구도를 흔듦
에이전트가 임의로 어려운 증명을 혼자 구성할 수 있다는 뜻은 아니지만, 모델은 큰 도움을 주며 더 많은 사람이 도구를 생산적으로 쓰게 함
형식 기법 사용이 이전보다 쉬워지면서, 과거의 비용 대비 효과 계산을 다시 검토할 가치가 생김
검증 병목이 더 중요해짐
- 모델은 유용한 코드를 점점 잘 작성하지만, 모델이 생성한 코드와 실제 릴리스할 수 있는 코드 사이에는 큰 차이가 있음
- 모델은 주어진 목표 달성에는 놀라울 정도로 뛰어나지만, 그 과정에서 코드베이스 품질을 유지하거나 개선하는 데에는 충분히 강하지 않음
- 에이전트가 만든 코드는 나아지고 있지만, 지나치게 복잡하고 이상한 버그와 경계 사례가 많으며 코드베이스의 핵심 불변식을 따르지 않는 경향이 있음
- 사람은 에이전트가 만든 코드가 충분한 품질인지 검증하는 데 많은 시간을 써야 함
- 형식 기법은 이 검증 부담을 줄이고 리뷰 과정을 더 효율적으로 만들 수 있음
에이전트는 피드백에서 강해짐
- 에이전트는 강화학습으로 훈련할 때와 코딩에 사용할 때 모두 피드백에서 이득을 얻음
- 형식 기법은 에이전트가 어려운 문제를 푸는 능력을 높일 수 있는 강력한 피드백 형태가 됨
- 테스트도 매우 가치 있으며, 속성 기반 테스트와 퍼징을 활용하면 더 좋아질 수 있음
- 테스트만으로는 충분하지 않고, 프로그램이 탐색할 수 있는 상태 공간을 덮는 데에는 본질적 한계가 있음
- OxCaml 프로그래밍 경험에서 에이전트는 타입 시스템이 주는 보편 보장에서 큰 이득을 얻음
- 타입 시스템이 데이터 레이스를 막을 수 있으면 데이터 레이스를 제거할 수 있음
- 타입을 잘 구성해 크로스 사이트 스크립팅 취약점을 불가능하게 만들면, 단순 테스트로는 어려운 방식으로 취약점을 없앨 수 있음
- 타입은 에이전트와 함께 프로그래밍할 때 검증 병목을 완화하고 더 나은 피드백을 제공함
- 더 강력한 증명 기법을 활용하면 추가적인 개선 여지가 생길 수 있음

왜 여기서 하는가

전 세계가 에이전트가 프로그래밍의 미래에 어떤 의미를 갖는지 생각하고 있으며, 형식 기법과 에이전트를 결합하려는 스타트업도 많음
Jane Street은 사용하는 언어를 깊게 통제할 수 있어, 증명 지향 기법에 더 적합하도록 언어를 조정할 수 있음
가능한 방향은 여러 가지임
- 속성의 모듈식 명세를 타입 시스템에 통합할 수 있음
- 소유권과 가변성 같은 요소에 타입 수준 제약을 추가해 특정 증명을 쉽게 만들 수 있음
- 증명 기법을 언어에 직접 넣을 수 있음
준비된 프로그래머 커뮤니티
- Jane Street에는 이런 기법을 받아들일 준비가 된 프로그래머 커뮤니티가 있음
- 프로그래밍 언어를 다루는 사람에게는 더 나은 프로그래밍 아이디어를 만드는 일보다, 그 아이디어를 실제 업무에 쓰게 만드는 일이 더 어려움
- Jane Street에서는 약속된 새롭고 낯선 타입 시스템 기능이 충분히 빨리 나오지 않는다는 이유로 사용자가 불만을 제기하는 일이 자주 있음
- 이런 기법을 활용할 배경을 가진 사람이 많고, 올바른 결과와 고품질 소프트웨어를 만드는 데 대한 관심도 이미 자리 잡고 있음
- 적극적이고 기대가 큰 사용자 기반은 단기 개선과 장기 비전을 함께 시도할 자유를 줌
- 단기 개선은 비교적 빠르게 영향을 줄 수 있음
- 장기 비전은 몇 년에 걸쳐 도달할 수 있는 더 야심 찬 목표가 됨
- 단기 시도에서 배우면서 장기 목표를 향해 구축할 수 있음
외부 도구와의 관계
- 외부 세계의 작업을 무시하지 않으며, 여러 프로그래밍 언어 커뮤니티의 작업에서 기대와 영감을 얻고 있음
- 관련 도구에는 Lean, Dafny, Rocq, Agda, Iris 등이 있음
- OxCaml을 일부 도구와 통합해 이미 존재하는 우수한 인프라를 활용할 방법을 찾고 있음
- 언어와 증명 기법을 동시에 다룰 때만 실현할 수 있는 고유한 장점도 있다고 봄