에이전트 코딩의 등장이 Jane Street의 형식 기법에 대한 시각을 어떻게 바꾸었는지, 그리고 왜 지금 형식 기법 팀을 꾸리고 있는지에 대한 글.
저는 지난 25년 동안 사람들에게 Jane Street라는 조직은 형식 기법에 관심이 없다고 말해 왔습니다.
이제는 더 이상 그렇게 말하지 않습니다.
그동안 우리가 틀렸다고 정확히 생각하게 되었다는 뜻은 아닙니다. 분명히 말하자면, 우리는 더 낫고 더 신뢰할 수 있는 코드를 작성하도록 도와주는 도구의 힘을 굳게 믿습니다. 그리고 타입 시스템은 우리가 엄청난 혜택을 얻어 온 일종의 경량 형식 기법입니다. 그래서 여러분은 우리가 더 본격적인 형식 기법의 열렬한 지지자였을 것이라고 예상할 수도 있습니다.
하지만 몇몇 특별한 경우를 제외하면(특히 하드웨어 합성), 우리의 판단은 형식 기법이 우리에게 그 비용만큼의 가치가 없다는 것이었습니다. 그리고 그 비용은 정말 큽니다! seL4는 이것의 훌륭한 예입니다. 그것은 형식적으로 검증된 마이크로커널이며, 대단한 업적입니다. 하지만, 세상에, 그걸 해내는 데 엄청난 비용이 들었습니다! 8,700줄의 C를 검증하는 데 25 인년의 노력이 들었고, 코드 한 줄마다 대략 23줄의 증명과 반 인일의 검증 시간이 필요했습니다.
우리의 바람은 오늘날 정교한 타입 시스템이 우리에게 그러하듯, 형식 기법을 소프트웨어를 구축하는 데 널리 유용한 도구로 만드는 것입니다.
그런 종류의 접근은 보안이 중요한 마이크로커널처럼 위험 부담이 크고 명세가 비교적 명확한 경우에는 가치가 있을 수 있습니다. 하지만 대부분의 소프트웨어에는 도무지 말이 되지 않으며, 우리에게는 가장 중요한 소프트웨어에조차도 맞지 않는다고 느껴졌습니다.
하지만 에이전트 코딩의 등장은 우리의 관점을 바꾸어 놓았고, 우리는 회의적인 태도에서 가능성에 대한 흥분으로 옮겨 왔습니다. 그리고 그 결과, 우리는 이제 형식 기법에 집중할 팀을 꾸리고 있습니다. 우리의 바람은 오늘날 정교한 타입 시스템이 우리에게 그러하듯, 형식 기법을 소프트웨어를 구축하는 데 널리 유용한 도구로 만드는 것입니다.
에이전트 코딩은 여러 면에서 형식 기법의 판을 흔들어 놓습니다.
우선, 그것은 형식 기법을 사용하는 비용을 극적으로 바꿉니다. 에이전트가 스스로 임의로 어려운 증명을 만들어낼 수 있다는 뜻은 아닙니다.1 하지만 모델은 엄청나게 도움이 되며, 이런 도구를 생산적으로 사용할 수 있는 사람들의 범위를 넓혀 줍니다. 형식 기법이 그 어느 때보다 사용하기 쉬워진 지금, 오래된 비용 대비 편익 계산을 다시 검토할 가치가 있습니다.
하지만 바뀐 것은 비용 측면만이 아닙니다. 이제는 편익도 더 커 보입니다. 여기에는 실제로 두 가지 이유가 있습니다.
검증 병목은 그 어느 때보다 중요해졌습니다. 모델은 유용한 코드를 작성하는 데 점점 더 능숙해지고 있습니다. 하지만 모델이 생성한 코드와 실제로 배포하고 싶은 코드 사이에는 큰 간극이 있습니다. 어느 정도는 이것이 모델이 학습되는 방식의 산물입니다. 모델은 눈앞에 제시된 목표를 달성하는 데는 놀라울 정도로 능하지만, 그 과정에서 코드베이스의 품질을 유지하고 심지어 개선하는 데는 그다지 뛰어나지 않습니다. 에이전트 코드는 점점 나아지고 있지만, 여전히 지저분한 쪽으로 기웁니다. 지나치게 복잡하고, 이상한 버그와 구석 사례로 가득하며, 자신이 속한 코드베이스의 핵심 불변식을 따르지 않는 경우가 많습니다.
그 결과, 사람들은 에이전트가 만들어낸 코드가 기준에 부합하는지 검증하는 데 많은 시간을 써야 합니다. 그리고 형식 기법은 그런 검증 부담의 일부를 덜고, 리뷰 과정을 훨씬 더 효율적으로 만드는 방법이 될 수 있습니다.
별개로, 에이전트는 피드백을 먹고 자랍니다. 이것은 RL을 사용해 에이전트를 훈련할 때도, 에이전트를 코딩에 사용할 때도 모두 사실입니다. 그리고 형식 기법은 어려운 문제를 해결하는 에이전트의 능력을 키워 줄 수 있는 또 하나의 강력한 피드백 형태입니다.
우리가 본격적인 형식 기법에 흥분하는 이유의 상당 부분은, 에이전트와 함께 프로그래밍할 때 타입이 얼마나 가치 있는지 보고 있기 때문입니다.
형식 기법만이 피드백을 얻는 유일한 방법이라는 뜻은 아닙니다. 테스트 또한 엄청나게 가치 있으며, property-based tests와 fuzzing을 적극 활용하면 더 좋아질 수 있습니다. 그리고 우리는 테스트 인프라를 구축하는 데 정말 많은 시간을 써 왔습니다.
하지만 테스트만으로는 충분하지 않습니다! 프로그램이 탐색할 수 있는 상태 공간을 테스트가 포괄하는 능력에는 본질적인 한계가 있습니다. 우리가 OxCaml에서 직접 프로그래밍하며 본 것 중 하나는, 에이전트가 타입 시스템이 제공하는 보편적 보장, 즉 ∀로부터 엄청난 도움을 받는다는 점입니다. 만약 여러분의 타입 시스템에 데이터 경쟁을 방지하는 방법이 있다면, 여러분은 모든2 데이터 경쟁을 없앨 수 있습니다. 크로스사이트 스크립팅 취약점을 불가능하게 만드는 방식으로 타입을 설계한다면, 단순한 테스트만으로는 하기 어려운 방식으로 그런 취약점을 정말로 완전히 없앨 수 있습니다.
실제로 우리가 본격적인 형식 기법에 흥분하는 이유의 상당 부분은, 에이전트와 함께 프로그래밍할 때 타입이 얼마나 가치 있는지 보고 있기 때문입니다. 검증 병목을 완화하는 데도, 에이전트에 더 나은 피드백을 제공하는 데도 그렇습니다. 그리고 그것은 더 강력한 증명 기법을 활용함으로써 얼마나 더 큰 도약이 가능할지 기대하게 만듭니다.
우리에게는 두 가지 강점이 있습니다. 우리가 사용하는 언어를 깊이 통제하고 있다는 점, 그리고 이를 받아들일 준비가 된 프로그래머 공동체가 있다는 점입니다.
여기서 생기는 한 가지 질문은 이것입니다. 왜 Jane Street가 이 문제에 잘 맞는 위치에 있는가? 전 세계가 에이전트가 프로그래밍의 미래에 무엇을 의미하는지 고민하고 있고, 형식 기법과 에이전트를 결합하는 방법을 찾는 스타트업도 셀 수 없이 많습니다. 왜 이것이 우리가 내부적으로 추진할 일일까요? 그리고 바깥세상의 형식 기법 전문가들은 왜 여기서 우리의 노력에 합류하는 일을 흥미롭게 여겨야 할까요?
우선, 우리는 우리가 사용하는 언어를 깊이 통제하고 있으며, 그 덕분에 그 언어를 증명 지향 기법에 더 적합한 터전으로 조정할 수 있습니다. 여기에는 여러 잠재적인 방향이 있습니다. 속성의 모듈식 명세를 타입 시스템에 통합하는 것부터, 특정 종류의 증명을 더 쉽게 만들기 위해 소유권이나 가변성과 같은 것에 관한 타입 수준 제약을 추가하는 것, 나아가 증명 기법을 언어 자체에 직접 내장하는 것까지 가능합니다.
또한 우리는 이를 받아들일 준비가 된 프로그래머 공동체를 갖고 있습니다, 또는 적어도 제가 접해 본 어떤 진지한 프로그래밍 공동체보다 더 준비되어 있습니다. 대부분의 프로그래밍 언어 연구자들에게 쉬운 부분은 프로그래밍을 더 좋게 만드는 새롭고 더 나은 아이디어를 떠올리는 일입니다. 어려운 부분은 그런 아이디어를 누군가가 실제 작업에 정말 사용하도록 설득하는 일입니다.
Jane Street에서는 상황이 다릅니다! 우리는 우리가 약속한 새롭고 이상한 타입 시스템 기능이 충분히 빨리 나오지 않는다고 화를 내는 사용자들을 일상적으로 봅니다. 우리는 이런 기법을 활용할 적절한 배경을 가진 사람들을 많이 보유하고 있으며, 일을 올바르게 하고 고품질 소프트웨어를 만들고자 하는 관심도 깊이 배어 있습니다.
우리는 이런 사용자 기반이 여러 접근법을 섞어 시도할 자유를 줄 것이라고 생각합니다. 우리가 단기간에 이룰 수 있다고 생각하는 개선도 있고, 그것은 꽤 즉각적인 영향을 줄 것입니다. 또 몇 년 안에 도달할 수 있는 곳에 대한 야심찬 장기 비전도 있습니다. 적극적으로 참여하고 흥분해 있는 사용자 기반이 있기에 이 두 접근 모두 가능해지고, 첫 번째 접근에서 배우면서 두 번째 접근을 향해 나아갈 수 있습니다.
그렇다고 해서 우리가 바깥세상의 작업을 무시하겠다는 뜻은 아닙니다. 우리는 Lean, Dafny, Rocq, Agda, Iris 같은 도구를 중심으로 한 다양한 다른 PL 공동체의 작업에서 큰 자극과 영감을 받고 있습니다. 그리고 이미 존재하는 훌륭한 인프라를 활용하기 위해 OxCaml을 이런 도구들 가운데 일부와 통합할 방법을 찾는 일도 기대하고 있습니다. 하지만 우리는 언어와 증명 기법을 동시에 다룸으로써만 실현할 수 있는 고유한 장점도 있다고 생각합니다.
이 이야기가 흥미롭게 들린다면, 지원을 고려해 보세요! 우리는 London과 New York 모두에서 사람을 찾고 있습니다. 우리는 지금 이 자리를 위한 면접과 팀 구성의 초기 단계에 있으며, 우리 앞에는 엄청난 양의 일이 놓여 있습니다. 그리고 여러분이 그 일부가 되어 주시길 바랍니다.
우리의 경험으로는, 복잡한 증명을 헤쳐 나가려면 모델은 여전히 인간의 도움과 지도가 필요합니다. 인간 프로그래머는 어떤 시스템이 왜 작동하는지, 그리고 높은 수준에서 그것을 어떻게 증명해 나갈지에 대한 아이디어를 가질 수 있습니다. 하지만 대부분의 프로그래머는 이런 증명 아이디어를 특정 증명 시스템이 만족할 수 있는 방식으로 어떻게 부호화해야 하는지 알지 못합니다. 모델은 그런 고된 작업의 상당 부분을 자동화할 수 있고, 증명을 실제로 써 내려가는 기술적 세부 사항에 대한 즉각적인 전문성의 원천을 제공할 수 있습니다.↩
좋아요, 음, 어쩌면 정말 전부는 아닐 수도 있습니다. Obj.magic 같은 탈출구가 있어서 타입 수준 제약을 우회할 수 있습니다. 하지만 코드의 대부분에 대해서는 그런 예외를 추적하고 금지할 수 있으며, 그러면 보편적 보장에 매우 가까운 무언가를 얻게 됩니다. 그리고 실제로 형식 기법은 그런 탈출구의 사용이 왜 실제로 안전한지 명시적으로 밝히게 해 줄 수도 있습니다.↩
Yaron Minsky는 2002년에 Jane Street에 합류했으며, 회사가 OCaml을 사용하기 시작하도록 설득한 사람이라는 다소 미심쩍은 영예를 자신이 차지하고 있다고 말합니다.
