# 형식 기법과 프로그래밍의 미래 > Clean Markdown view of GeekNews topic #30511. Use the original source for factual precision when an external source URL is present. ## Metadata - GeekNews HTML: [https://news.hada.io/topic?id=30511](https://news.hada.io/topic?id=30511) - GeekNews Markdown: [https://news.hada.io/topic/30511.md](https://news.hada.io/topic/30511.md) - Type: GN+ - Author: [neo](https://news.hada.io/@neo) - Published: 2026-06-16T00:36:44+09:00 - Updated: 2026-06-16T00:36:44+09:00 - Original source: [blog.janestreet.com](https://blog.janestreet.com/formal-methods-at-jane-street-index/?from_theconsensus=1) - Points: 1 - Comments: 1 ## Topic Body - **형식 기법**은 소프트웨어가 의도한 성질을 만족하는지 증명하는 도구이며, 에이전트 코딩 확산으로 비용·효용 판단이 달라지고 있음 - Jane Street은 과거 형식 기법이 일부 특수 사례를 제외하면 비용 대비 가치가 낮다고 봤지만, 이제 **전담 팀**을 만들고 있음 - seL4는 8,700줄 C 코드 검증에 25인년이 들었고, 코드 한 줄마다 약 23줄의 증명과 반 인일 검증이 필요했음 - 에이전트가 생성한 코드는 출시 가능한 품질과 차이가 있으며, **검증 병목**을 줄이고 에이전트에 강한 피드백을 주는 수단으로 형식 기법이 중요해짐 - Jane Street은 언어를 깊게 통제할 수 있고 준비된 프로그래머 커뮤니티가 있어, **OxCaml**과 증명 지향 기법을 함께 발전시킬 여지가 있다고 봄 --- ### 형식 기법과 프로그래밍의 미래 - Jane Street은 지난 25년 동안 조직 차원에서 **형식 기법**에 관심이 없다고 말해 왔지만, 이제는 그 입장을 유지하지 않음 - 더 나은 코드와 더 신뢰할 수 있는 코드를 쓰기 위한 도구의 힘은 오래전부터 중시해 왔고, 타입 시스템은 큰 이득을 준 가벼운 형식 기법으로 여겨짐 - 특수 사례, 특히 하드웨어 합성을 제외하면 형식 기법은 비용이 너무 커서 대부분의 소프트웨어에 맞지 않는다고 판단해 왔음 - [seL4](https://sel4.systems/)는 형식 검증된 마이크로커널이자 중요한 성취였지만, 8,700줄 C 코드 검증에 25인년이 들었음 - 코드 한 줄마다 약 23줄의 증명이 필요했고, 한 줄 검증에 약 반 인일이 필요했음 - 보안이 중요한 마이크로커널처럼 위험이 크고 명세가 비교적 명확한 경우에는 이런 접근이 가치 있을 수 있음 - 대부분의 소프트웨어에는 맞지 않았고, Jane Street의 가장 중요한 소프트웨어에도 맞지 않는다고 느껴졌음 - 에이전트 코딩의 등장이 판단을 바꾸었고, 형식 기법 가능성에 대한 회의가 기대감으로 전환됨 - Jane Street은 **형식 기법 팀**을 만들고 있으며, 정교한 타입 시스템만큼 널리 유용한 소프트웨어 구축 도구로 만들기를 기대함 ### 왜 마음이 바뀌었나 - 에이전트 코딩은 여러 방식으로 **형식 기법**의 기존 비용·효용 구도를 흔듦 - 에이전트가 임의로 어려운 증명을 혼자 구성할 수 있다는 뜻은 아니지만, 모델은 큰 도움을 주며 더 많은 사람이 도구를 생산적으로 쓰게 함 - 형식 기법 사용이 이전보다 쉬워지면서, 과거의 비용 대비 효과 계산을 다시 검토할 가치가 생김 - ## 검증 병목이 더 중요해짐 - 모델은 유용한 코드를 점점 잘 작성하지만, 모델이 생성한 코드와 실제 릴리스할 수 있는 코드 사이에는 큰 차이가 있음 - 모델은 주어진 목표 달성에는 놀라울 정도로 뛰어나지만, 그 과정에서 코드베이스 품질을 유지하거나 개선하는 데에는 충분히 강하지 않음 - 에이전트가 만든 코드는 나아지고 있지만, 지나치게 복잡하고 이상한 버그와 경계 사례가 많으며 코드베이스의 핵심 불변식을 따르지 않는 경향이 있음 - 사람은 에이전트가 만든 코드가 충분한 품질인지 검증하는 데 많은 시간을 써야 함 - 형식 기법은 이 **검증 부담**을 줄이고 리뷰 과정을 더 효율적으로 만들 수 있음 - ## 에이전트는 피드백에서 강해짐 - 에이전트는 강화학습으로 훈련할 때와 코딩에 사용할 때 모두 **피드백**에서 이득을 얻음 - 형식 기법은 에이전트가 어려운 문제를 푸는 능력을 높일 수 있는 강력한 피드백 형태가 됨 - 테스트도 매우 가치 있으며, [속성 기반 테스트](https://harrisongoldste.in/papers/icse24-pbt-in-practice.pdf)와 [퍼징](https://blog.janestreet.com/getting-from-tested-to-battle-tested/)을 활용하면 더 좋아질 수 있음 - 테스트만으로는 충분하지 않고, 프로그램이 탐색할 수 있는 상태 공간을 덮는 데에는 본질적 한계가 있음 - [OxCaml](http://oxcaml.org) 프로그래밍 경험에서 에이전트는 타입 시스템이 주는 **보편 보장**에서 큰 이득을 얻음 - 타입 시스템이 데이터 레이스를 막을 수 있으면 데이터 레이스를 제거할 수 있음 - 타입을 잘 구성해 크로스 사이트 스크립팅 취약점을 불가능하게 만들면, 단순 테스트로는 어려운 방식으로 취약점을 없앨 수 있음 - 타입은 에이전트와 함께 프로그래밍할 때 검증 병목을 완화하고 더 나은 피드백을 제공함 - 더 강력한 증명 기법을 활용하면 추가적인 개선 여지가 생길 수 있음 ### 왜 여기서 하는가 - 전 세계가 에이전트가 프로그래밍의 미래에 어떤 의미를 갖는지 생각하고 있으며, 형식 기법과 에이전트를 결합하려는 스타트업도 많음 - Jane Street은 사용하는 언어를 **깊게 통제**할 수 있어, 증명 지향 기법에 더 적합하도록 언어를 조정할 수 있음 - 가능한 방향은 여러 가지임 - 속성의 모듈식 명세를 타입 시스템에 통합할 수 있음 - 소유권과 가변성 같은 요소에 타입 수준 제약을 추가해 특정 증명을 쉽게 만들 수 있음 - 증명 기법을 언어에 직접 넣을 수 있음 - ## 준비된 프로그래머 커뮤니티 - Jane Street에는 이런 기법을 받아들일 준비가 된 **프로그래머 커뮤니티**가 있음 - 프로그래밍 언어를 다루는 사람에게는 더 나은 프로그래밍 아이디어를 만드는 일보다, 그 아이디어를 실제 업무에 쓰게 만드는 일이 더 어려움 - Jane Street에서는 약속된 새롭고 낯선 타입 시스템 기능이 충분히 빨리 나오지 않는다는 이유로 사용자가 불만을 제기하는 일이 자주 있음 - 이런 기법을 활용할 배경을 가진 사람이 많고, 올바른 결과와 고품질 소프트웨어를 만드는 데 대한 관심도 이미 자리 잡고 있음 - 적극적이고 기대가 큰 사용자 기반은 단기 개선과 장기 비전을 함께 시도할 자유를 줌 - 단기 개선은 비교적 빠르게 영향을 줄 수 있음 - 장기 비전은 몇 년에 걸쳐 도달할 수 있는 더 야심 찬 목표가 됨 - 단기 시도에서 배우면서 장기 목표를 향해 구축할 수 있음 - ## 외부 도구와의 관계 - 외부 세계의 작업을 무시하지 않으며, 여러 프로그래밍 언어 커뮤니티의 작업에서 기대와 영감을 얻고 있음 - 관련 도구에는 [Lean](https://lean-lang.org/), [Dafny](https://dafny.org/), [Rocq](https://rocq-prover.org/), [Agda](https://hackage.haskell.org/package/Agda), [Iris](https://iris-project.org/) 등이 있음 - OxCaml을 일부 도구와 통합해 이미 존재하는 우수한 인프라를 활용할 방법을 찾고 있음 - 언어와 증명 기법을 동시에 다룰 때만 실현할 수 있는 **고유한 장점**도 있다고 봄 ### 합류 안내 - Jane Street은 [London](https://www.janestreet.com/join-jane-street/position/8588405002/)과 [New York](https://www.janestreet.com/join-jane-street/position/8585303002/)에서 형식 기법 관련 인력을 찾고 있음 - 현재 해당 자리의 인터뷰와 팀 구축은 초기 단계임 - 앞으로 해야 할 일이 매우 많고, 팀에 합류할 사람을 찾고 있음 ### 보충 - 모델은 복잡한 증명을 다룰 때 여전히 사람의 도움과 지도가 필요함 - 사람 프로그래머는 시스템이 왜 작동하는지, 높은 수준에서 어떻게 증명할지에 대한 아이디어를 가질 수 있음 - 대부분의 프로그래머는 특정 증명 시스템을 만족시키는 방식으로 증명 아이디어를 인코딩하는 방법을 알지 못함 - 모델은 증명을 작성하는 기술적 세부 사항에서 많은 반복 작업을 자동화하고 전문성을 제공할 수 있음 - `Obj.magic` 같은 탈출구는 타입 수준 제약을 우회하게 만들 수 있음 - 대부분의 코드에서 이런 예외를 추적하고 금지하면 보편 보장에 매우 가까운 상태를 얻을 수 있음 - 형식 기법은 이런 탈출구 사용이 실제로 안전한 이유를 명시적으로 만들 수 있음 ## Comments ### Comment 59696 - Author: neo - Created: 2026-06-16T00:36:46+09:00 - Points: 1 ###### [Hacker News 의견들](https://news.ycombinator.com/item?id=48526633) - 수십 년 전에 **정확성 증명** 작업을 했고, 당시 시스템이 이후의 많은 시스템보다 증명 자동화가 더 많았음 쉬운 부분은 최초의 SAT 솔버인 Oppen-Nelson 단순화기가 해결했고, 어려운 부분은 휴리스틱과 이전 보조정리를 쓰는 Boyer-Moore 증명기가 맡았음. 사람의 어려운 일은 증명기가 시도해보고 이후 증명에 쓸 **보조정리**를 제안하는 것이었음 이후 시스템들은 자동화가 줄어든 듯했고, 형식 기법이 빗나간 이유는 실무보다 형식주의에 너무 빠졌기 때문이라고 봄. 상업 프로젝트에서 버그 없는 코드를 원했던 입장에서는, 학계식 프로젝트가 논문용 간결한 표기와 적은 경우 분석을 선호하는 수학자 편향에 빠졌다고 느꼈음 실제로는 많은 자동화된 갈아넣기가 필요하고 통찰은 적게 필요해야 함. 영리한 사람들이 종이와 연필 증명의 장황함을 피하려고 양상 논리, 시간 논리 같은 새 논리를 계속 만들었지만 별로 도움이 되지 않았음. 이 분야의 기본 진실은 대부분의 정리가 꽤 평범하다는 것임 Jane Street 사람들이 말하듯 **언어를 통제할 수 있다는 점**이 큰 장점임. 검증 문장은 프로그래밍 언어 안에 통합되어야 하고, 주석이나 다른 문법, 별도 파일에 박혀 있으면 불필요한 일이 늘어남. Jane Street가 이 방향을 밀어붙이는 건 좋아 보임 40년도 더 전에 너무 일찍 이 일을 했고, 당시에는 Boyer-Moore 증명기로 숫자 이론을 처음부터 쌓는 데 계산 시간이 45분쯤 걸렸지만 이제는 1초도 안 걸림 [https://archive.org/details/manualzilla-id-5928072/page/n3/m...]() - 형식 기법을 오래 해온 입장에서, 새 논리가 도움이 안 된다는 말에는 조금 동의하기 어려움. 산업용 논리는 실용적이고, 시스템이 만족해야 할 정교한 속성을 매우 간결하게 쓸 수 있게 해줌 논리는 컴퓨터 과학과 소프트웨어 공학에서 물리학·기계공학·토목공학의 미적분 같은 위치에 있음. LTL이나 최근의 **분리 논리** 같은 것들은 엄청난 돌파구였음 인기를 꽤 얻은 **TLA+** 가 그 증거이고, 모델 검사는 매우 실용적임. 지금 흥미로운 점은 더 무거운 형식 기법, 특히 정리 증명이 일반 시스템 소프트웨어에서도 쓸 만큼 저렴해질 수 있다는 것임 함수에 대한 형식 명세를 쓰고 SAT/SMT, 정리 증명기, LLM의 하이브리드로 합성하고 정확성을 증명받는 방식이 머지않아 표준이 될 수도 있음 On the Unusual Effectiveness of Logic in Computer Science: [https://www.cs.rice.edu/~vardi/papers/aaas99.jsl.pdf]() From Philosophical to Industrial Logics: [https://www.cs.rice.edu/~vardi/papers/icla09.pdf]() - 형식 명세에서는 **사람이 해석하고 작성할 수 있음**이 정말 중요해질 것임 걱정되는 건 해독하기 어려운 수학이 생기고, 소수의 신봉자 집단이 그것을 지키는 상황임. 서로 다른 난해한 표기들은 호환되지 않고, 하나를 이해해도 다른 것을 이해하는 데 별 도움이 안 될 수 있음. 대부분은 제대로 검증할 수 없는 영어 문장만 쓰게 될 것임 더 나쁘게는 기계에게 자기 문장을 형식화하게 해놓고, 그 형식주의나 증명은 이해하지 못한 채 **검증 연극**에 참여하다가 모든 것이 터지면 놀라는 척할 수도 있음 - **Ada/SPARK**를 봤는지 궁금함. 봤다면 일이 어떻게 되어야 하는지에 대한 직관과 맞는지도 궁금함 타입 시스템이 빠르게 다루지 못하는 부분에 이런 능력을 통합하려는 작업을 천천히 하고 있어서, 이 길을 먼저 가본 사람들의 관점이 관심 있음 - 좋음. 최근 몇 달 동안 Scala 3에서 **표현력 높은 타입**을 써서 타입이 점점 더 많은 컴파일 시간 증명을 담도록 옮겨왔음. 매크로는 쓰지 않지만 몇 개는 쓸 만함 이 방식은 에이전트형 테스트가 퍼져나가는 문제를 줄이는 데만 도움이 되는 게 아니라, 에이전트가 낮은 품질의 작업 방식으로 떨어지는 것도 막는 듯함. 특히 에이전트가 합리적으로 일반화해야 할 때도 모든 것에 새 단형 타입을 만들려는 **명사 축적**을 막고 있음 좋은 품질의 에이전트 코딩을 가속하는 쪽은 형식 기법을 닮은 도구들, 강한 타입 시스템을 가진 언어까지 포함한 쪽이라고 봄 여기서 표현력 높은 타입이란, 팀이 이미 타입 수준 프로그래밍에 익숙하지 않다면 일반 코드베이스에 넣고 싶지는 않은 기법들을 뜻함. 즉 고차 종류 타입과 타입 함수가 이상한 물건이 아니라 기본 블록인 팀이어야 함 에이전트는 지식 면에서 대부분의 개발자보다 “수학”을 잘하고, 범주론에 물든 개발자보다도 나은 경우가 많음. 더구나 대화에 대해 “무한한” 인내심이 있다고 보면 교육도 꽤 잘함 개인적으로는 Codex에게 취미 증명 몇 개를 Lean식으로 바꾸게 했는데 매우 쉬웠음. 100% “정확하다”고 말하는 건 아니고, 더 철저히 확인하려면 Lean 4를 더 배워야 하지만, 기본적으로 고전적인 증명 함정도 점검하는 듯함. 형식 기법의 미래가 매우 기대됨 - Gen AI가 코드를 많이 만들기 때문에 인간의 가치를 **검증** 쪽으로 옮기자는 이야기로 보임. 프로그래밍이 정말 무엇인지 가끔 생각함 영어가 모국어가 아닌 입장에서는 프로그래밍을 배우는 것 자체가 큰 도전임. 번역되지 않은 영어 문서를 이해하려면 기계번역에 의존해야 하고, 내 언어로 된 자료는 5~6년쯤 뒤처져 있음 이제 AI가 만든 수만 줄의 코드를 코드 리뷰하는 게 불가능하니, 수학적 증명 같은 절대 규칙을 세우자는 논의가 보임. 이 글을 읽으니 Rust의 borrow checker가 떠오름. 실제로 Rust를 몇 번 써보면 사람들이 borrow checker를 피하려고 꼼수를 쓰는 나쁜 습관으로 이어지곤 함 수학적 엄밀성이 지나치면 사람은 우회로를 찾게 됨. 나처럼 교육이 부족한 프로그래머는 특히 그러기 쉬움 이런 시도는 결국 특정한 형식화된 답만을 위한 코드를 쓰는 결과가 될 것 같음. 그렇게 표준화되면 인간의 요구에 대응할 수 있을지 확신이 안 섬 이런 방어적 프로그래밍 시도는 괜찮지만, 내가 만든 표현으로는 **공격적 프로그래밍**을 하고 싶음. 위험을 감수하되 빨리 고치고 배포하며, 시간이 지나면 충분히 좋아질 것이라고 믿는 방식임 물론 Jane Street처럼 정확도가 중요하고 업무 범위가 잘 정의된 기존 산업에서는 이 글의 접근이 맞음. 시장의 요구를 적절히 모델링할 만큼 데이터가 충분하기 때문임 하지만 돈을 벌려고 금광을 찾아 계속 이동하는 나 같은 사회적 패배자에게는 이런 방법론이 사치처럼 보임. 성숙한 모델링을 갖춘 기존 사업은 고학력의 전문 인력이 계속 최적화해야 하는데, 현실적으로 그 수요를 따라갈 수 없다는 걸 알고 있음. 그래서 모델링이 구조화되지 않은 곳을 찾지만, 거기서도 이 접근을 쓸 수 있을지는 모르겠음 - Jane Street의 관점에서 봐야 함. 그들은 **고빈도 거래** 회사이고 주식과 금융상품을 수백만, 어쩌면 수천만 단위로 거래함 거기에는 “고치면 된다”가 없음. 무엇이 잘못됐는지 이해할 때쯤이면 이미 수십억을 잃었을 수 있음 그래서 공격적 방식은 비핵심 영역에서는 통할 수 있음 참고로 이미 곳곳에서 방어적 방식을 쓰고 있음. Python, Java 등에는 가비지 컬렉터가 있고, 코드가 의도대로 실행된다는 점이 검증되는 셈임 언제쯤 형식 검증이 보이기 시작할지 궁금했는데, 구현 세부사항을 걱정하는 단계에서 문제를 과학적·수학적으로 서술하는 단계로 가는 건 자연스러움 - “공격적 프로그래밍”이라는 표현이 좋음. 다만 그 패러다임은 이미 업계의 **기본 상태**임 Gen AI 때문에 방어적 프로그래밍의 비용은 크게 내려갔고, 인간 검증의 비용은 크게 올라갔음. 반면 형식 기법은 검증을 싸게 만들지만, 명세·타입·증명을 쓰고 구현을 단단한 틀에 맞춰 구부리는 등 구현 오버헤드가 큼 그런데 Gen AI가 그 힘든 작업을 자동화할 수 있음. 둘은 천생연분임 - 번역되지 않은 영어 문서를 기계번역에 의존한다면, 주제와는 조금 벗어나지만 **영어를 배우는 것**을 강하게 추천함 약간의 노력이 필요하지만, 계속되는 번역 오버헤드를 없애면 엄청난 도움이 될 것임 - 이런 방법론이 사치라는 데 동의함. 글에서도 그 점을 인정하고 있고, Jane Street는 이 접근에서 이익을 얻기에 꽤 **특수하게 준비된 조직**임 - Jane Street가 자신들에게 관련 있어서 그런 글을 낸 건 당연하고, 모든 프로그래밍에 일반적으로 적용되지 않는 것도 당연함 다만 스스로를 “사회적 패배자”라고 하거나 커리어에서 이런 실천을 따르지 않는다는 점이 이 논점과 어떻게 관련되는지는 잘 모르겠음 - 최근 관련 아이디어를 가지고 놀고 있는데, 놀라웠던 건 **최전선 모델**, 특히 ChatGPT-5.5가 Roqc, 예전 Coq 증명 보조기에서 특정 수동 증명을 얼마나 잘 완성하느냐였음 증명이 항상 예쁘진 않지만, ChatGPT는 제한적이지만 0은 아닌 증명 보조기 경험과 증명되는 보조정리 분야의 꽤 큰 도메인 경험을 가진 내가 훨씬 오래 걸릴 일을 몇 분, 10~100회 반복 안에 증명하는 경우가 많음 이 짧은 글의 맥락에서 이게 흥미로운 이유는 특정 형식 기법 도구가 동작하는 기본 가정을 흔들기 때문임. Frama-C, Ada/SPARK 등은 CVC5, Z3 같은 도구가 자동으로 해소할 수 있는 증명 의무를 생성하는 데 집중하고, 실패하면 Roqc에서 수동 증명하는 꽤 고통스러운 대안으로 넘어감 흔한 흐름은 어떤 의무가 “어렵다”, 즉 자동으로 해소되지 않는다는 걸 발견한 뒤, 코드의 의무 생성 지점에서 보이는 보조정리와 단언 집합을 재구성해 “쉽게” 만들거나, 심지어 코드를 바꾸는 것임 Roqc 증명이 두 배로 비싼 세계에서는 말이 됨. 사람에게 작성이 어렵고, 코드와 주변 증명이 변할 때 유지보수 변동도 크기 때문임 하지만 Roqc 증명이 “AI가 루프에 들어간 자동 해소”가 된다면 이 비용 차이가 사라짐. 그러면 증명을 코드처럼 쓸 수 있고, 사람이 읽기 쉬운 명료함을 1순위로, 컴파일러나 증명기 최적화는 한참 뒤로 둘 수 있음. 그 함의는 아직 완전히 소화하지 못했지만 꽤 흥미로움 - 요구사항이 바뀌어서 증명할 수 없는 상황에서, AI가 증명을 쉽게 만들려고 **코드와 요구사항을 바꿔버릴** 가능성은 얼마나 될까 증명은 다뤄본 적 없지만, “변경 후 이 테스트가 실패했다”고 말하면 AI가 내 의도인 기존 테스트와 새 테스트를 모두 통과하도록 코드를 고치는 대신 테스트 자체를 바꿔버리는 일은 가끔 봤음 - 내 경험과 비슷하지만, 나는 Lean을 골랐음. 만들고 싶던 기능과 더 관련이 컸음 앞으로가 기대됨 - ChatGPT가 Roqc 증명을 몇 분과 10~100회 반복 안에 해낸다고 할 때, 그 **증명 자체가 올바른지**는 어떻게 아는지 궁금함 - 형식 명세 이야기를 읽을 때마다 “같은 테스트를 다른 방식으로 쓰는 것”처럼 보이고, 더 나쁘게는 “같은 구현을 다른 방식으로 쓰는 것”처럼 보임 두 번 작성하면 오류를 잡는 데 도움이 될 수는 있겠지만, 형식 명세도 테스트나 구현과 똑같은 버그를 가질 수 있다면 무엇이 특별한지 잘 모르겠음 근본 문제는 프로그램이 뭔가를 한다는 걸 형식적으로 증명하려면 그 “뭔가”를 매우 구체적으로 정의해야 한다는 데 있음. 그러면 사실상 테스트나 구현을 다시 쓰는 것처럼 됨 몇 년 동안 이 주제를 간헐적으로 들여다봤고, 뭔가 놓치고 있다는 느낌이 계속 드는데 그게 뭔지 모르겠음. 누가 설명해줄 수 있을까 - Dijkstra의 유명한 말처럼, “프로그램 테스트는 버그의 존재를 보일 수는 있지만, 부재를 보일 수는 없다” 테스트의 결함은 문제가 될 수 있다고 생각한 동작만 테스트할 수 있다는 점임. 잘못될 수 있다는 걸 몰랐던 동작까지 선제적으로 고치려면 도구상자의 더 특이한 도구가 필요함. 퍼즈 테스트가 그 방향의 한 시작이고, **형식 검증**도 또 다른 시작임 물론 이런 도구의 품질은 원하는 동작은 허용하고 원하지 않는 동작은 금지하는 포괄적인 형식 모델을 얼마나 잘 쓰느냐에 달려 있고, 여러 분야에서 우리는 여전히 놀랄 만큼 그 지점에서 멀리 있음 - 큰 차이는 형식 기법이 **모든 것에 대해**라는 전칭 한정자를 쓸 수 있게 해준다는 점임 예를 들어 단위 테스트에서는 “foo('abc')가 뒤쪽 공백이 없는 문자열을 반환한다”고 쓸 수 있음 하지만 형식 기법으로는 “임의의 입력 x에 대해 foo(x)가 뒤쪽 공백이 없는 문자열을 반환한다”고 증명할 수 있음 사소한 예지만, “임의의 프로그램 P에 대해 compile(P)는 P와 같은 동작을 한다” 같은 더 복잡한 것도 상상할 수 있음 물론 “같은 동작”이 무엇인지는 정의해야 함 - 소프트웨어는 안 쓰지만 ASIC과 FPGA 설계에서는 형식 기법 명세가 SAT 솔버 같은 도구를 써서 대상 설계가 명세를 만족하는지 판단하게 해줌 설계의 속성을 지정하면 도구가 다양한 방식으로 설계를 테스트해 그 속성을 위반할 수 있는지 확인함 예를 들어 교통 신호를 제어하는 시스템이라면, 서로 교차하는 차선이 동시에 또는 일정 시간 안에 둘 다 초록불이 될 수 없다는 속성을 지정할 수 있음 도구는 이를 **완전 탐색**으로 확인하고, 위반하는 코드 추적을 보여줄 수 있음 - 단순히 “같은 테스트를 다른 방식으로 쓰는 것” 이상임. 각 테스트는 대체로 독립적이거나 관리 불가능하게 커지고, 테스트 묶음의 완전성을 분기 커버리지 같은 비교적 거친 겹침 방식으로 따져야 함 정적으로 증명되는 타입 시스템은 각 구성 요소가 다른 모든 요소와 미리 맞춰 검사되도록 해줌. 단순히 “이 테스트가 통과한다”가 아니라, 조합했을 때 “이 모든 테스트가 합리적이고 일관된 전체를 만든다”를 보장하고, 일관되지 않은 모델이 코드에 구현되는 것을 막음 Rust의 `match`가 가능한 모든 분기를 완전히 다루도록 요구하는 것을 코드베이스 전체 규모로 확대한 예와 비슷함 근본적인 논리나 이론 오류를 만들면 잡아주지 못한다는 점은 맞음. 하지만 예컨대 Haskell 타입 시스템, 임시 함수형 테스트, 속성 테스트를 합친 것보다 훨씬 견고하다는 데 놀랄 수 있음. 그것도 전체적으로는 강한 체계라고 보지만, 형식적으로 증명된 암호학은 훨씬 높은 기준임 - 강력한 차이는 특정 테스트와 **전수 증명** 사이에 있음. 경계 조건 테스트를 떠올리지 못하면 그대로 놓침. 좋은 모델이 있으면 배포 전에 그 존재를 알고 고칠 수 있음 특히 동시성·분산·다중 스레드 상황에서 가치가 큼. 경쟁 조건과 교착 상태는 테스트하고 추론하기 매우 어렵고, “A, B, C가 A, C, B 순서로 일어날 수 있는가” 같은 문제가 그렇음 이 분야의 성숙은 대략 이렇게 갈 것 같음. 첫째, LLM이 처음에는 “두 번째로 해보기”식 사후 검증에 그치더라도 형식 기법의 학습과 사용을 훨씬 빠르게 할 것임 둘째, “구현 코드가 바뀌었는데 모델을 깨뜨린 것처럼 보이나?”를 LLM이 확인하는 자동화로 이동할 것임. 여전히 결정적이지는 않지만, 가끔만 바뀌는 무언가를 사람이 리뷰해야 하는 것보다는 훨씬 나을 가능성이 큼 셋째, 진짜 도약은 “형식 명세만 쓰고 구현은 생성하라”는 도구를 다음 단계로 끌어올리는 데 있을 것임. 이런 코드 생성 프로젝트는 이미 여럿 있지만 대부분 회사들이 원하는 수준까지 완전히 익지 않았음. LLM 도구가 그중 하나를 필요에 맞추는 데 드는 1~2년의 수작업을 가속할 수 있다면 어떨까 - Kleppmann의 이전 글 [https://martin.kleppmann.com/2025/12/08/ai-formal-verificati...]()도 참고할 만하고, 타입 시스템이나 린터에 넣을 수 있는 것은 당연히 그렇게 할지 저울질해야 함 더 쓰기 편한 방식이 나오길 바람. 글에 나온 도구 중에는 dafny와 iris가 산업용에 가장 가까운 듯함. Amazon S3도 내부에서 TLA를 써온 이력이 있는 것으로 앎 하지만 이 분야의 **TypeScript 같은 존재**, 기존 도구에 자연스럽게 들어가고 비용 없는 추상화처럼 작동하며 사람들이 진심으로 예전 방식보다 선호하는 무언가는 아직 못 본 것 같음 커스텀 린터를 쓰는 것도 여전히 꽤 별로임. golangci-lint는 고통스러운 코드베이스이고, semgrep은 안 써봤지만 규칙 엔진이 위압적으로 보였음. 마음에 드는 AST API도 아직 못 써봄 - 연역적 추론, 즉 “형식 기법”에 대한 이런 찬가는 늘 그 근본 한계를 빠뜨림. **공리와 정의가 대상 도메인에 얼마나 잘 맞는가**라는 문제임 “이론상 이론과 실제는 차이가 없다. 실제로는…”이라는 말과 같음. Jane Street는 코드의 목적이 결정적 알고리즘을 구현하는 것이라 매핑이 1:1인 큰 코드베이스를 유지할 것이라고 추측함. 많은 개발자가 그런 영역에서 일하지만, 수백만 명은 그렇지 않음. 대부분의 UI, 대부분의 탐색적 작업 등이 그렇음 형식 기법과 나란히, 논리·수학적 방식은 아니지만 승인 기준을 높은 해상도로 정의하려는 흐름도 있음. 이 흐름은 적어도 매핑 문제와 씨름하지만, 지도가 영토가 아닌 대부분의 곳에서는 해결하지 못함 Google 검색 결과 페이지는 극도로 진화한 내부 최적화 프레임워크를 갖췄지만 정말 최적점에 도달했을까? 흐릿한 아이디어를 잡으려고 급히 만든 프로토타입이 더 잘 보여줄 수도 있었을까? 이런 질문은 시스템 내부가 아니라 그 시스템이 섬기는 바깥을 보아야 가장 잘 답할 수 있음 - 형식 기법은 정확히 **의미론이 잘 정의된 도메인**을 위한 것임 논리 회로, 형식 검증이 많이 들어가는 CPU 구성요소, 커널, 프로토콜, 파서, 컴파일러, 암호학, 보안 프레임워크, 동시성 기본 요소 등은 검증에서 큰 이익을 얻음 - 실제 대부분의 UI는 결국 상태 기계로 귀결되고, 이는 형식 검증에 매우 잘 맞음 더 배우려면 Hillel Wayne의 글이 좋은 출발점임: [https://www.hillelwayne.com/formally-specifying-uis/]() - Google 결과 페이지 자체는 잘 정의되어 있지 않지만, 그 아래 코드의 아마 **90% 이상**은 잘 정의되어 있을 것임 그리고 어떤 경우에는 결과가 잘 정의되어 있지 않아도 학습할 수 있으므로, 무엇이 말이 될지 앉아서 생각하는 문제만은 아님 - 프로그래밍 언어의 설계와 구현에 조금 관심 있는 입장에서 이 문장이 정말 흥미로웠음. “프로그래밍 언어를 다루는 대부분의 사람에게 쉬운 부분은 프로그래밍을 더 좋게 만들 새롭고 더 나은 아이디어를 내는 것이다. 어려운 부분은 누군가가 그 아이디어를 실제 일에 쓰도록 설득하는 것이다” 완전히 동의함. 이득이 있더라도 새 언어에 넣을 수 있는 **낯섦의 양**에는 한계가 있음 하지만 AI 에이전트는 프로그래밍 언어 설계의 급진적으로 새로운 아이디어에 큰 저항을 느끼지 않을 것임. 에이전트형 AI 이후 프로그래밍 언어 설계가 어떻게 진화할지 한동안 생각해왔음 채택 걱정을 훨씬 덜 할 수 있을 때, 프로그래밍 언어를 개선하기 위해 어떤 새 아이디어를 만들 수 있을지 보는 것은 매우 흥미로울 것 같음 [https://steveklabnik.com/writing/the-language-strangeness-bu...]() - 애플리케이션 보안 테스트 쪽에서 **형식 기법**을 적용하는 방향으로 작업 중이고, 같은 접근을 비즈니스 로직 검증에도 적용할 수 있다고 봄 이를 위해 taint analysis를 쓰고 있음. 꽤 잘 확립된 형식 기법 접근이지만, 실제 코드베이스의 데이터 흐름 복잡성 때문에 현장에서는 아직 널리 적용되지 않았음 형식 기법을 AST 패턴 매칭과 단순한 타입 검사 너머로 확장하는 건 정말 어려운 작업임. taint analysis로 실제 코드베이스의 절차 간 데이터 흐름을 몇 분 안에 추적하고 깊이 숨은 취약점을 찾는 수준에 도달하기까지 수년의 연구개발이 걸렸음 관심 있으면 프로젝트를 볼 수 있음: [https://github.com/seqra/opentaint]() - 약 18개월 전에 LLM과 함께 타입을 쓰는 데 빠졌고, `lean4`에 진지해진 건 6~8개월 전쯤임. 이제는 실용적인 C/C++ FFI, 따라서 사실상 모든 것과 연결되는 `CIC` 증명 기반 없이는 소프트웨어 작업에 AI 보조를 쓰는 걸 고려하지도 않음 JSON부터 Python까지 모두 금지했고, `nix`도 컴파일러가 있도록 다시 썼음. 우리가 쓰는 거의 모든 것은 속성 테스트와 여러 퍼즈 테스트를 한계까지 거칠 뿐 아니라, 최소한 `.olean` 연결을 통해 속성 테스트를 구동하는 `lean4` 증명을 갖고 있음. 여유가 있으면 도메인 전체의 완전성까지 증명하고 그 속성도 테스트함 빠른 부분은 모두 `lean4`에서 생성되므로 C++/Rust 논쟁은 건너뜀. C++의 버그가 실제로는 `lean4` 코드의 버그일 때 장점이 있지만, 어느 쪽으로도 갈 수 있음 큰 변화이고, “JSON과 Python을 금지한다고?”라며 회의적인 사람을 탓하지는 않음. 하지만 우리는 이런 방식으로 수백만 줄을 검사했고, **AI + 형식 시스템**은 AI 없음에서 AI와 Python으로 가는 것보다 훨씬 더 큰 도약임. 후자는 우리의 경험상 진전이 단조롭지 않지만, 전자는 거의 항상 단조롭게 나아감 꽤 과감한 일도 가능함. 이것은 ISL과 CuTe 같은 것들이 모델링하는 다면체 텐서 계산의 형식 증명이고, 이를 이용하면 C++23의 `mdspan`으로 장치에서 swizzling과 tiling을 하고 그것이 맞다는 것도 증명할 수 있음. 다만 이 예시는 커버리지에 대한 L'Hopital식 논증을 잘 보여주지는 않음: [https://github.com/b7r6/mdspan-cute]() 그 결과는 정말 빠르고, 첫 시도부터 빠름 [https://straylight.software/assets/lambda-hierarchy.svg]() - Agda와 Idris 2를 CIC 아래에 둔 것은 **람다 계층도**를 좋게 봐도 오해하게 만듦 - 그래서 어떤 소프트웨어를 만들었고, 왜 유용한지 궁금함