▲

의존형을 왜 사용하지 않는가

 (lawrencecpaulson.github.io)
1P by GN⁺ 19시간전 | ★ favorite | 댓글 1개
  • 의존형(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) 과는 다름
▲
GN⁺ 19시간전  [-]
Hacker News 의견

  • 의존형(dependent types) 은 특정 상황에서 매우 유용함
    예를 들어 Python이 “10×5 크기의 float32 행렬”을 타입으로 표현하고 타입체크할 수 있으면 좋겠다고 생각함
    하지만 Curry–Howard 대응처럼 증명과 타입을 동일시하는 개념은 인간 입장에서 혼란스러움
    타입 오류는 단순히 수정 가능한 실수로 느껴지지만, 증명 오류는 훨씬 복잡하고 사고가 필요한 문제임
    그래서 Lean의 진짜 강점은 타입 시스템이 아니라 커뮤니티와 mathlib의 오픈소스 구조라고 봄
    Isabelle의 AFP가 학술지처럼 운영되는 반면, Lean은 pull request 기반의 협업이 활발함
    현재 나는 새로운 정리 증명기 Acorn(acornprover.org)을 개발 중이며, Lean과 Isabelle의 장점을 결합하려 함
    Lean의 단순한 의존형 표현력은 좋지만, 너무 깊게 사용하면 디버깅이 어려워짐

    • C++이나 Rust에서도 상수 크기의 배열이라면 이런 타입 표현이 가능함
      다만 런타임에만 알려지는 인덱스의 범위를 컴파일 타임에 보장할 수는 없음
      진정한 의존형 언어는 런타임 에러를 타입 수준에서 방지할 수 있음
    • Rust의 const generics나 C++의 non-type template parameter로도 충분히 가능함
      실제로 의존형 언어에서도 런타임 오류 방지를 위해 의존형을 쓰는 경우는 드물고,
      주로 데이터 구조 불변식이나 프로그램 정의 후의 검증에 사용됨
      관련 참고: division-by-zero in type theory FAQ, Xavier Leroy 발표자료
    • TypeScript에서도 약간의 의존형 흉내를 낼 수 있음
      예를 들어 이 코드의 38번째 줄처럼 타입으로 행렬 크기를 표현할 수 있음
      벡터 타입 정의나
      행렬 곱셈 결과 타입도 구현했음
      다만 개인 프로젝트 수준에서 실험 중이며, 대규모 데이터 프로젝트에는 적합하지 않을 수도 있음
    • “증명이 타입과 동일하다”는 표현이 흥미로움
      이는 Propositions as Types 개념과 관련 있음
      런타임에서 의존형이 어떻게 동작하는지, 컴파일과 런타임 타입체크가 모두 필요한지 궁금함
      구현 시 간접 참조가 많아지는 복잡성이 생기지 않을까 하는 의문이 있음
    • “Python에서 10×5 행렬 타입을 표현하고 싶다”는 말은, 결국 클래스로 직접 정의하면 된다는 뜻 아님?

  • Dr. Paulson의 주장은 의존형이 나쁘다는 게 아니라 필수는 아니라는 점임
    Lean의 성능 문제나 의도적 동치(intensional equality) 관련 논의가 더 있었으면 좋았을 것 같음
    Isabelle의 HEq(링크)처럼 정의적 동치가 아닌 경우가 문제를 일으킴
    그래서 나는 의존형을 가능한 한 적게 쓰는 게 낫다고 생각함
    ACL2처럼 정적 타입이 없는 시스템에서도 충분히 검증이 가능함
    결국 중요한 건 실용성과 검증 가능성의 균형임

    • 소프트웨어 검증 관점에서는 Isabelle(비의존형)도 충분히 강력함
      Lean이나 Agda는 아직 산업 규모의 검증에는 덜 쓰임
      Concrete Semantics(링크)와 Logical Verification 2025(링크)를 비교해보는 것도 흥미로움
      현실적으로는 refinement types가 더 실용적일 수 있음
      예: Rust Creusot, Dafny, LiquidHaskell의 leftpad 증명 예시
    • 수학에서는 증명을 프로그램으로 쓰지 않기 때문에 의존형이 잘 작동함
      하지만 프로그램 검증에서는 “두 증명이 동일하다” 같은 복잡한 보조정리(lemma) 가 필요해지고, 이는 증명 불가능한 경우가 많음
    • “의존형을 가능한 한 적게 써야 한다”는 이유가 궁금함
    • “필요하지 않다”는 주장은 회피처럼 들림
      중요한 건 기능이 얼마나 유용한가이지, 존재의 필요성 여부가 아님
      결국 도구 선택은 개발자 취향과 효율성의 문제임

  • 현대 논리학 논쟁의 상당 부분이 미적 선호로 귀결된다는 점이 흥미로움
    실질적 이점이 압도적이었다면 논쟁이 없었을 것임
    참고로 Paulson과 Lamport의 1999년 논문 “Typing in Specification Languages”는 좋은 읽을거리임
    이후 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)를 사용 중이며, MongoDB보다 빠르고 복잡한 데이터 모델링에 유용함
    Palantir의 ontology 개념과도 유사함

    • “비희석(non-dilutive) 성장 엔진을 구축한다”는 문구를 좀 더 구체적으로 설명해줄 수 있는지 궁금함
    • TypeDB를 선택한 이유와 실제 성능 수치가 궁금함

  • 결국 의존형의 비밀은 언제 사용하지 말아야 하는지를 아는 것 같음
    Lean이나 Rocq를 비판하기보다는, 상황에 따라 Isabelle 스타일로 접근할 수도 있지 않을까 생각함

  • Paulson 연구팀의 형식화 프로젝트 Alexandria(링크)가 인상적임
    특히 양자 컴퓨팅 알고리즘 형식화 연구(논문 링크)가 흥미로움

  • 예전엔 의존형이 미래라고 믿었지만, 실제 프로젝트에서는 생산성 저하가 컸음
    지금은 명확하고 유지보수 쉬운 솔루션을 더 선호함
    팀이 이해하고 확장 가능한 도구라면 그게 좋은 도구임

  • 나는 완전한 의존형보다는 그 경계에 있는 타입 시스템을 좋아함
    예를 들어 Purescript는 Haskell보다 강력한 row-type을 기본 제공하고,
    타입 수준 리스트, 문자열, 정규식까지 지원함
    이를 typeclass 기반 논리 프로그래밍 방식으로 활용할 수 있음

답변달기