# 의존형을 왜 사용하지 않는가 > Clean Markdown view of GeekNews topic #24116. Use the original source for factual precision when an external source URL is present. ## Metadata - GeekNews HTML: [https://news.hada.io/topic?id=24116](https://news.hada.io/topic?id=24116) - GeekNews Markdown: [https://news.hada.io/topic/24116.md](https://news.hada.io/topic/24116.md) - Type: GN+ - Author: [neo](https://news.hada.io/@neo) - Published: 2025-11-04T04:33:16+09:00 - Updated: 2025-11-04T04:33:16+09:00 - Original source: [lawrencecpaulson.github.io](https://lawrencecpaulson.github.io//2025/11/02/Why-not-dependent.html) - Points: 1 - Comments: 1 ## Topic Body - **의존형(type theory)** 은 증명 객체를 포함하지만, 저자는 이를 **불필요하고 비효율적인 구조**로 평가함 - **AUTOMATH**와 **Martin-Löf 형식 체계** 등 과거 의존형 기반 시스템을 직접 연구했으나, **Isabelle**은 **일반적(generic) 논리 프레임워크**로 발전함 - **단순형 이론(higher-order logic)** 을 기반으로 한 Isabelle/HOL은 **자동화·대규모 라이브러리·가독성**에서 강점을 보임 - **ALEXANDRIA 프로젝트**를 통해 고차 논리만으로도 **고급 수학 정리의 형식화**가 가능함을 입증 - Lean 등 의존형 시스템의 성숙에도 불구하고, **성능 문제와 복잡성** 때문에 저자는 여전히 **고차 논리 접근법의 실용성**을 선호함 --- ### 의존형과 증명 객체 - 의존형 이론에서는 **증명 객체(proof objects)** 가 필수적이지만, 저자는 이를 **공간 낭비**로 간주 - LCF 구조에서는 **논리 내부가 아닌 구현 언어 수준의 타입 검사**로 정당한 증명 단계만 실행 가능 - Robin Milner의 통찰로 **proof kernel** 개념이 도입되어 Isabelle의 기반이 됨 - 저자는 “의존형을 사용하지 않았다”는 질문에 대해 “**오랫동안 사용했다**”고 답함 ### AUTOMATH 경험 - 1977년 Caltech에서 **N. G. de Bruijn**의 AUTOMATH 강의를 들었으며, 시스템 자체는 직접 사용하지 못함 - 당시 **Eindhoven 대학 시스템**이 ARPAnet에 연결되지 않았고, **ALGOL 60 기반 컴퓨터**가 필요했기 때문 - AUTOMATH는 **의존형 시스템**이지만 **Curry–Howard 대응**을 구현하지 않음 - 사용자가 원하는 논리의 **기호와 추론 규칙을 공리로 추가**해야 했음 - de Bruijn은 이를 “**모든 음식을 제공하는 큰 레스토랑**”에 비유 - Isabelle은 이 개념을 이어받아 **논리 프레임워크로서의 일반성**을 추구 - 그러나 de Bruijn은 **집합론을 혐오**하고 수학을 본질적으로 **타입 기반**으로 보았음 - 저자는 AUTOMATH의 **정당성 검증**을 질문했고, de Bruijn은 **언어 이론서(300쪽)** 를 보냈으나 만족스럽지 않았음 ### Martin-Löf 형식 이론 - **Göteborg의 Chalmers 대학**에서 **Martin-Löf 형식 이론**을 연구하며 **프로그램 합성** 가능성에 매료됨 - **Heyting의 직관주의 논리** 원리를 직접 구현한 점에서 “옳음”이 명확하다고 평가 - 수년간 연구를 진행하며 **Isabelle의 초기 버전**을 Martin-Löf 이론으로 구현 - 현재도 **Isabelle/CTT**로 배포에 포함됨 - 그러나 **Per Martin-Löf 중심의 교조적 분위기**와 **강제된 내재적 동치(intensional equality)** 전환으로 연구가 무너짐 - 이후 등장한 **Calculus of Constructions(CoC)** , **Rocq**, **Lean** 등도 같은 의문을 남김 - CoC는 수십 년간 여러 변형과 선택적 공리를 거듭함 ### 연구 선택과 Isabelle의 방향 - 연구자들은 **새로운 형식 체계 개발**과 **기존 체계의 확장 활용** 중 선택해야 함 - Isabelle은 **일반화된 프레임워크**로 설계되어 다양한 논리를 수용 - 1985년 **Mike Gordon**은 **Church의 단순형 이론**으로 하드웨어 검증을 수행 - 이후 **John Harrison**이 벡터 차원 인코딩을 고안 - Isabelle/HOL은 Church 이론에 **공리적 타입 클래스**와 **locale 모듈 시스템**을 추가 - Lean 커뮤니티는 CoC 기반으로 **방대한 수학 형식화(mathlib)** 를 달성 ### ALEXANDRIA 프로젝트와 고차 논리의 한계 실험 - **ERC 지원 ALEXANDRIA 프로젝트**는 Isabelle의 **자동화·라이브러리·가독성**을 강조 - 초기에는 고차 논리로는 한계가 있을 것이라 예상했으나, 실제로는 **Grothendieck 스킴** 등 고급 수학도 성공적으로 형식화 - **Paulo Emílio de Vilhena**와 **Martin Baillon**이 **모든 체가 대수적으로 닫힌 확장을 가짐**을 증명 - 프로젝트는 **Balog–Szemerédi–Gowers 정리** 등 고급 결과까지 확장 - “의존형 없이는 수학 형식화가 불가능하다”는 주장은 사라지고, “의존형이 더 깔끔하다”는 주장만 남음 ### Lean과 의존형에 대한 현재 입장 - Lean의 **커뮤니티 규모**와 **Blueprint 도구**는 부럽지만, **성능 문제와 복잡성**은 여전 - **intensional equality**와의 충돌, **의존형 사용 시기 판단의 어려움**이 반복적으로 보고됨 - 저자는 의존형을 **Tesla의 완전자율주행(Full Self-Driving)** 에 비유하며, **과도한 기대와 실제 불편함**을 지적 ### 부록: 고차 논리의 이론적 한계 - 일부에서는 고차 논리가 **증명 이론적으로 약하다**고 주장하지만, 이는 **ZF 집합론 대비 약함**을 의미할 뿐 - **ALEXANDRIA 결과**에 따르면, 고차 논리로도 **Grothendieck 스킴 등 복잡한 수학 구조**를 다룰 수 있음 - 단 두 개의 증명만이 **ZF 공리 추가**를 필요로 했으며, 이는 **ZF 객체를 직접 언급하는 정리**였음 ### 각주 - **직관주의**는 언어를 단순한 기록 수단으로 보는 철학으로, 오늘날의 **구성적 수학(constructive mathematics)** 과는 다름 ## Comments ### Comment 45828 - Author: neo - Created: 2025-11-04T04:33:17+09:00 - Points: 1 ###### [Hacker News 의견](https://news.ycombinator.com/item?id=45790827) - **의존형(dependent types)** 은 특정 상황에서 매우 유용함 예를 들어 Python이 “10×5 크기의 float32 행렬”을 타입으로 표현하고 타입체크할 수 있으면 좋겠다고 생각함 하지만 **Curry–Howard 대응**처럼 증명과 타입을 동일시하는 개념은 인간 입장에서 혼란스러움 타입 오류는 단순히 수정 가능한 실수로 느껴지지만, 증명 오류는 훨씬 복잡하고 사고가 필요한 문제임 그래서 Lean의 진짜 강점은 타입 시스템이 아니라 **커뮤니티와 mathlib의 오픈소스 구조**라고 봄 Isabelle의 AFP가 학술지처럼 운영되는 반면, Lean은 pull request 기반의 협업이 활발함 현재 나는 새로운 정리 증명기 **Acorn**([acornprover.org](https://acornprover.org))을 개발 중이며, Lean과 Isabelle의 장점을 결합하려 함 Lean의 단순한 의존형 표현력은 좋지만, 너무 깊게 사용하면 디버깅이 어려워짐 - C++이나 Rust에서도 상수 크기의 배열이라면 이런 타입 표현이 가능함 다만 런타임에만 알려지는 인덱스의 범위를 컴파일 타임에 보장할 수는 없음 진정한 의존형 언어는 **런타임 에러를 타입 수준에서 방지**할 수 있음 - Rust의 const generics나 C++의 non-type template parameter로도 충분히 가능함 실제로 의존형 언어에서도 런타임 오류 방지를 위해 의존형을 쓰는 경우는 드물고, 주로 **데이터 구조 불변식**이나 프로그램 정의 후의 검증에 사용됨 관련 참고: [division-by-zero in type theory FAQ](https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/), [Xavier Leroy 발표자료](https://www.cs.ox.ac.uk/ralf.hinze/WG2.8/26/slides/xavier.pdf) - TypeScript에서도 약간의 의존형 흉내를 낼 수 있음 예를 들어 [이 코드](https://github.com/AKST/analysis-notebook/blob/main/lib/base/math/type.ts)의 38번째 줄처럼 타입으로 행렬 크기를 표현할 수 있음 [벡터 타입 정의](https://github.com/AKST/analysis-notebook/blob/777acf427c65c2a76647af0487a4c1acc5527604/lib/base/math/value.d.ts#L140)나 [행렬 곱셈 결과 타입](https://github.com/AKST/analysis-notebook/blob/777acf427c65c2a76647af0487a4c1acc5527604/lib/base/math/value.d.ts#L175)도 구현했음 다만 개인 프로젝트 수준에서 실험 중이며, 대규모 데이터 프로젝트에는 적합하지 않을 수도 있음 - “증명이 타입과 동일하다”는 표현이 흥미로움 이는 **Propositions as Types** 개념과 관련 있음 런타임에서 의존형이 어떻게 동작하는지, 컴파일과 런타임 타입체크가 모두 필요한지 궁금함 구현 시 **간접 참조가 많아지는 복잡성**이 생기지 않을까 하는 의문이 있음 - “Python에서 10×5 행렬 타입을 표현하고 싶다”는 말은, 결국 클래스로 직접 정의하면 된다는 뜻 아님? - Dr. Paulson의 주장은 의존형이 나쁘다는 게 아니라 **필수는 아니라는 점**임 Lean의 성능 문제나 **의도적 동치(intensional equality)** 관련 논의가 더 있었으면 좋았을 것 같음 Isabelle의 HEq([링크](https://lean-lang.org/doc/reference/latest/Basic-Propositions/Propositional-Equality/#HEq))처럼 정의적 동치가 아닌 경우가 문제를 일으킴 그래서 나는 의존형을 가능한 한 적게 쓰는 게 낫다고 생각함 ACL2처럼 정적 타입이 없는 시스템에서도 충분히 검증이 가능함 결국 중요한 건 **실용성과 검증 가능성의 균형**임 - 소프트웨어 검증 관점에서는 Isabelle(비의존형)도 충분히 강력함 Lean이나 Agda는 아직 산업 규모의 검증에는 덜 쓰임 **Concrete Semantics**([링크](http://concrete-semantics.org))와 **Logical Verification 2025**([링크](https://github.com/lean-forward/logical_verification_2025))를 비교해보는 것도 흥미로움 현실적으로는 **refinement types**가 더 실용적일 수 있음 예: Rust Creusot, Dafny, LiquidHaskell의 [leftpad 증명 예시](https://github.com/hwayne/lets-prove-leftpad) - 수학에서는 증명을 프로그램으로 쓰지 않기 때문에 의존형이 잘 작동함 하지만 프로그램 검증에서는 “두 증명이 동일하다” 같은 **복잡한 보조정리(lemma)** 가 필요해지고, 이는 증명 불가능한 경우가 많음 - “의존형을 가능한 한 적게 써야 한다”는 이유가 궁금함 - “필요하지 않다”는 주장은 회피처럼 들림 중요한 건 기능이 **얼마나 유용한가**이지, 존재의 필요성 여부가 아님 결국 도구 선택은 **개발자 취향과 효율성**의 문제임 - 현대 논리학 논쟁의 상당 부분이 **미적 선호**로 귀결된다는 점이 흥미로움 실질적 이점이 압도적이었다면 논쟁이 없었을 것임 참고로 Paulson과 Lamport의 1999년 논문 [“Typing in Specification Languages”](https://www.cl.cam.ac.uk/~lp15/papers/Reports/lamport-paulson-types.pdf)는 좋은 읽을거리임 이후 Lamport의 TLA+처럼 **비형식적 형식주의**도 발전했음 - 나는 이것을 단순한 미학의 문제가 아니라 **트레이드오프의 문제**로 봄 컴파일 타임 보장이라는 이점을 얻는 대신, 복잡성과 빌드 시간 증가라는 대가를 치름 결국 “그 교환이 가치 있는가”가 핵심임 - HOL(단순형 이론)의 문제는 의존성이 아니라 **논리적 강도 부족**임 이는 Zermelo 집합론의 제한된 버전과 동등하며, 현대 수학을 완전히 형식화하기엔 약함 특히 **범주론(category theory)** 같은 분야의 크기 문제를 다루기 어려움 - Isabelle의 **locales 기능**을 이용해 Grothendieck 스킴을 형식화한 사례가 있음 실제 수학자들의 스타일과 얼마나 다른지 궁금함 - 논리적 강도를 높이려면 **공리 추가**도 가능함 예를 들어 ‘inaccessible cardinal’을 추가하면 타입 이론의 ‘universe’ 개념과 유사해짐 - 나는 형식 방법(formal methods) 전공이었고 의존형을 멋지다고 생각했지만, 실제 사용은 **항상 uphill battle**이었음 F#을 쓸 때 F* 도입을 시도했지만, 동료들이 수학적 학습 곡선을 부담스러워함 결국 **수학이 들어간 도구는 엔지니어들이 잘 배우지 않는다**는 냉소적 결론에 도달함 - F*는 수학보다는 **소프트웨어 검증 중심**이라 Lean과는 결이 다름 SMT 기반 제약 해결을 활용해 **가벼운 의존형 사용**이 가능함 하지만 “이게 정말 옳은가”라는 철학적 질문에는 답하지 못함 수학 증명과 소프트웨어 검증의 세계는 꽤 다름 - 사람들은 새로운 걸 배우지 않는 게 아니라, **투자 대비 효용이 낮다고 판단**할 뿐임 결국 시간은 한정되어 있음 - 우리 회사 **Phosphor**에서는 의존형을 데이터베이스/그래프 쿼리와 결합해 실험 중임 RDF의 한계를 보완하고, **논리 기반 쿼리 시스템**을 만들 수 있었음 실제로는 **TypeDB**([typedb.com](https://typedb.com))를 사용 중이며, MongoDB보다 빠르고 복잡한 데이터 모델링에 유용함 Palantir의 ontology 개념과도 유사함 - “비희석(non-dilutive) 성장 엔진을 구축한다”는 문구를 좀 더 구체적으로 설명해줄 수 있는지 궁금함 - TypeDB를 선택한 이유와 실제 **성능 수치**가 궁금함 - 결국 의존형의 비밀은 **언제 사용하지 말아야 하는지를 아는 것** 같음 Lean이나 Rocq를 비판하기보다는, 상황에 따라 Isabelle 스타일로 접근할 수도 있지 않을까 생각함 - Paulson 연구팀의 **형식화 프로젝트 Alexandria**([링크](https://www.cl.cam.ac.uk/~lp15/Grants/Alexandria/))가 인상적임 특히 **양자 컴퓨팅 알고리즘 형식화 연구**([논문 링크](https://link.springer.com/article/10.1007/s10817-020-09584-7))가 흥미로움 - 예전엔 의존형이 미래라고 믿었지만, 실제 프로젝트에서는 **생산성 저하**가 컸음 지금은 명확하고 유지보수 쉬운 솔루션을 더 선호함 팀이 이해하고 확장 가능한 도구라면 그게 좋은 도구임 - 나는 완전한 의존형보다는 그 **경계에 있는 타입 시스템**을 좋아함 예를 들어 **Purescript**는 Haskell보다 강력한 row-type을 기본 제공하고, 타입 수준 리스트, 문자열, 정규식까지 지원함 이를 **typeclass 기반 논리 프로그래밍 방식**으로 활용할 수 있음