의존형(dependent types) 은 특정 상황에서 매우 유용함
예를 들어 Python이 “10×5 크기의 float32 행렬”을 타입으로 표현하고 타입체크할 수 있으면 좋겠다고 생각함
하지만 Curry–Howard 대응처럼 증명과 타입을 동일시하는 개념은 인간 입장에서 혼란스러움
타입 오류는 단순히 수정 가능한 실수로 느껴지지만, 증명 오류는 훨씬 복잡하고 사고가 필요한 문제임
그래서 Lean의 진짜 강점은 타입 시스템이 아니라 커뮤니티와 mathlib의 오픈소스 구조라고 봄
Isabelle의 AFP가 학술지처럼 운영되는 반면, Lean은 pull request 기반의 협업이 활발함
현재 나는 새로운 정리 증명기 Acorn(acornprover.org)을 개발 중이며, Lean과 Isabelle의 장점을 결합하려 함
Lean의 단순한 의존형 표현력은 좋지만, 너무 깊게 사용하면 디버깅이 어려워짐
C++이나 Rust에서도 상수 크기의 배열이라면 이런 타입 표현이 가능함
다만 런타임에만 알려지는 인덱스의 범위를 컴파일 타임에 보장할 수는 없음
진정한 의존형 언어는 런타임 에러를 타입 수준에서 방지할 수 있음
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 기반 논리 프로그래밍 방식으로 활용할 수 있음
Hacker News 의견
의존형(dependent types) 은 특정 상황에서 매우 유용함
예를 들어 Python이 “10×5 크기의 float32 행렬”을 타입으로 표현하고 타입체크할 수 있으면 좋겠다고 생각함
하지만 Curry–Howard 대응처럼 증명과 타입을 동일시하는 개념은 인간 입장에서 혼란스러움
타입 오류는 단순히 수정 가능한 실수로 느껴지지만, 증명 오류는 훨씬 복잡하고 사고가 필요한 문제임
그래서 Lean의 진짜 강점은 타입 시스템이 아니라 커뮤니티와 mathlib의 오픈소스 구조라고 봄
Isabelle의 AFP가 학술지처럼 운영되는 반면, Lean은 pull request 기반의 협업이 활발함
현재 나는 새로운 정리 증명기 Acorn(acornprover.org)을 개발 중이며, Lean과 Isabelle의 장점을 결합하려 함
Lean의 단순한 의존형 표현력은 좋지만, 너무 깊게 사용하면 디버깅이 어려워짐
다만 런타임에만 알려지는 인덱스의 범위를 컴파일 타임에 보장할 수는 없음
진정한 의존형 언어는 런타임 에러를 타입 수준에서 방지할 수 있음
실제로 의존형 언어에서도 런타임 오류 방지를 위해 의존형을 쓰는 경우는 드물고,
주로 데이터 구조 불변식이나 프로그램 정의 후의 검증에 사용됨
관련 참고: division-by-zero in type theory FAQ, Xavier Leroy 발표자료
예를 들어 이 코드의 38번째 줄처럼 타입으로 행렬 크기를 표현할 수 있음
벡터 타입 정의나
행렬 곱셈 결과 타입도 구현했음
다만 개인 프로젝트 수준에서 실험 중이며, 대규모 데이터 프로젝트에는 적합하지 않을 수도 있음
이는 Propositions as Types 개념과 관련 있음
런타임에서 의존형이 어떻게 동작하는지, 컴파일과 런타임 타입체크가 모두 필요한지 궁금함
구현 시 간접 참조가 많아지는 복잡성이 생기지 않을까 하는 의문이 있음
Dr. Paulson의 주장은 의존형이 나쁘다는 게 아니라 필수는 아니라는 점임
Lean의 성능 문제나 의도적 동치(intensional equality) 관련 논의가 더 있었으면 좋았을 것 같음
Isabelle의 HEq(링크)처럼 정의적 동치가 아닌 경우가 문제를 일으킴
그래서 나는 의존형을 가능한 한 적게 쓰는 게 낫다고 생각함
ACL2처럼 정적 타입이 없는 시스템에서도 충분히 검증이 가능함
결국 중요한 건 실용성과 검증 가능성의 균형임
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) 같은 분야의 크기 문제를 다루기 어려움
실제 수학자들의 스타일과 얼마나 다른지 궁금함
예를 들어 ‘inaccessible cardinal’을 추가하면 타입 이론의 ‘universe’ 개념과 유사해짐
나는 형식 방법(formal methods) 전공이었고 의존형을 멋지다고 생각했지만, 실제 사용은 항상 uphill battle이었음
F#을 쓸 때 F* 도입을 시도했지만, 동료들이 수학적 학습 곡선을 부담스러워함
결국 수학이 들어간 도구는 엔지니어들이 잘 배우지 않는다는 냉소적 결론에 도달함
SMT 기반 제약 해결을 활용해 가벼운 의존형 사용이 가능함
하지만 “이게 정말 옳은가”라는 철학적 질문에는 답하지 못함
수학 증명과 소프트웨어 검증의 세계는 꽤 다름
결국 시간은 한정되어 있음
우리 회사 Phosphor에서는 의존형을 데이터베이스/그래프 쿼리와 결합해 실험 중임
RDF의 한계를 보완하고, 논리 기반 쿼리 시스템을 만들 수 있었음
실제로는 TypeDB(typedb.com)를 사용 중이며, MongoDB보다 빠르고 복잡한 데이터 모델링에 유용함
Palantir의 ontology 개념과도 유사함
결국 의존형의 비밀은 언제 사용하지 말아야 하는지를 아는 것 같음
Lean이나 Rocq를 비판하기보다는, 상황에 따라 Isabelle 스타일로 접근할 수도 있지 않을까 생각함
Paulson 연구팀의 형식화 프로젝트 Alexandria(링크)가 인상적임
특히 양자 컴퓨팅 알고리즘 형식화 연구(논문 링크)가 흥미로움
예전엔 의존형이 미래라고 믿었지만, 실제 프로젝트에서는 생산성 저하가 컸음
지금은 명확하고 유지보수 쉬운 솔루션을 더 선호함
팀이 이해하고 확장 가능한 도구라면 그게 좋은 도구임
나는 완전한 의존형보다는 그 경계에 있는 타입 시스템을 좋아함
예를 들어 Purescript는 Haskell보다 강력한 row-type을 기본 제공하고,
타입 수준 리스트, 문자열, 정규식까지 지원함
이를 typeclass 기반 논리 프로그래밍 방식으로 활용할 수 있음