▲

왜 그냥 Lean만 쓰지 않나요?

 (lawrencecpaulson.github.io)
1P by GN⁺ 5시간전 | ★ favorite | 댓글 1개
  • 수학 형식화의 역사는 Lean으로 시작되지 않았고, 거의 60년 전부터 여러 계보의 시스템이 핵심 기법과 성과를 이미 축적해 옴
  • 1968년의 AUTOMATH, LCF 계열, HOL, Rocq, ACL2, Mizar 같은 도구들은 실해석학부터 소수 정리, 네 가지 색 정리, Kepler 추측까지 폭넓은 형식화를 이뤄 냄
  • Lean은 큰 라이브러리와 활발한 공동체를 바탕으로 현대 수학 정의를 빠르게 쌓아 올렸지만, propositions as types나 의존 타입이 proof assistant의 유일한 길은 아님
  • Isabelle은 강한 자동화, 높은 가독성, 의존 타입 회피를 장점으로 내세우며, proof object 없이도 커널의 추상화 장벽으로 증명 검사를 구성하는 LCF 전통을 잇고 있음
  • AI가 구조화된 증명을 정리하고 다른 시스템으로 번역하는 흐름까지 더해지면서, 한 도구만 절대적 기준으로 보는 부담은 앞으로 더 줄어들 수 있음

초기 시스템과 다른 계보들

  • AUTOMATH

    • AUTOMATH는 1968년에 이미 수학 형식화에 필요한 요소 대부분을 포함했음
    • 1977년 Jutting은 AUTOMATH로 Landau의 Foundations of Analysis를 형식화했고, 순수 논리에서 출발해 복소수 구성까지 다룸
    • 동치류와 유리수 집합을 사용했고, 실수선의 Dedekind 완비성도 형식적으로 증명함
    • 이 성과는 20년 동안 다시 나오지 않았고, 1990년대 중반에야 John Harrison의 HOL Light와 Jacques Fleuriot의 Isabelle/HOL에서 다시 실수 형식화가 이뤄짐
    • 표기법은 매우 불편했고 자동화도 전혀 없어 증명이 길고 읽기 어려웠음
    • 그럼에도 동치류를 다루는 데서는 Rocq보다 낫다고 보며, Rocq 사용자들이 겪는 setoid hell과 달리 Jutting은 동치류 형식화를 차분하게 수행함

  • Boyer와 Moore

LCF 이후의 흐름

  • Edinburgh LCF는 프로그래밍 언어 이론에 집중했지만, 증명 도우미의 메타언어로 함수형 언어를 두는 발상은 널리 퍼짐
  • Cambridge, INRIA, Cornell 등 여러 그룹이 ML을 사용해 초기 HOL, Coq(현 Rocq), Nuprl 같은 도구를 만듦
  • HOL 그룹은 하드웨어 검증에 집중했지만, 부동소수점 하드웨어 검증 때문에 실해석학이 필요해졌음
  • John Harrison은 Cauchy 적분 공식을 통해 소수 정리 같은 본격적인 수학 결과를 HOL 계열에서 증명함
  • 100 theorems를 가능한 많이 검증하려는 목표 아래 HOL Light는 자주 최상위권에 올랐음
  • 2014년까지 이 계열 시스템들은 여러 고급 정리를 형식화했음
  • 이 정리들은 대체로 증명이 길고 복잡했고, 형식화 작업도 매우 큰 규모였으며, 정리에 남아 있던 의문을 줄이는 데 핵심 역할을 함

Lean 공동체의 부상

  • 수학자들은 앞선 형식화 성과들이 Grothendieck schemes나 perfectoid spaces 같은 주류 현대수학의 정교한 구성까지는 다루지 못했다고 봤음
  • Tom Hales는 이런 정의들을 라이브러리로 쌓아 올리는 방향을 택했고, 증명보다 정의의 축적에 초점을 두며 Lean을 선택함
  • 그는 Big Proof 프로그램에서 이 방향을 발표했고, 비슷한 구상도 함께 논의됨
  • Kevin Buzzard가 이를 듣고 교육에 Lean을 써보기로 하면서 이후 확산이 빨라짐
  • Lean 공동체의 중요한 전환점으로, Rocq를 오래 지배한 구성적 증명 집착에서 벗어난 점이 제시됨
  • 직관주의는 Russell의 역설 이후 등장했고, 실수 개념에도 특정한 함의를 가졌음
  • Martin-Löf type theory는 분명히 직관주의적 형식주의이지만 Rocq는 그렇게 단순하게 볼 수 없다고 적음
  • 그럼에도 Rocq 관련 논문들에서는 구성적 증명이 무관하거나 무의미한 자리에서도 반복적으로 등장했고, 이런 경향이 Rocq의 수학 적용을 가로막으면서 자리를 Lean에 넘겨줬다고 봄

propositions as types와 LCF의 차이

  • Propositions as types는 논리 기호 ∀, ∃, →, ∧, ∨ 와 타입 생성자 Π, Σ, →, ×, + 를 연결하는 이중성임
  • 이 틀은 아름답고 이론적으로 생산적이지만 유일한 길은 아님
  • proof assistant를 propositions as types 원리로 증명을 검사하는 소프트웨어로 한정하면, 지난 반세기 연구의 대부분이 정의 밖으로 밀려남
  • 그렇게 되면 Rocq, Lean, Agda만 남게 됨
  • AUTOMATH조차 propositions as types의 사례는 아니며, Π와 → 비슷한 요소는 있어도 논리는 일반 논리 교재처럼 공리들로 설정함
  • de Bruijn은 50년 전에 이미 타입과 명제의 분리가 필요하다고 봤음
  • 대표적으로 나눗셈은 세 인자를 받아야 하고, (x/y)의 값은 (y \ne 0)의 증명에 의존하게 되므로 proof irrelevance가 필요하다고 적음
  • LCF 접근이 propositions as types와 같다는 인식도 사실과 다르다고 못박음
  • Rocq와 Lean에는 명제의 sort인 Prop가 있으며, 여기서는 같은 명제의 모든 증명 객체가 같은 값으로 평가돼 proof irrelevance를 제공함
  • 그렇다고 거대한 증명 객체가 사라지는 것은 아니며 실제 시스템에는 여전히 남아 있음
  • Robin Milner의 핵심 발견은 LCF에서 증명 객체 자체가 필요 없다는 점이었음
  • ML의 추상 데이터 타입 안에 증명 커널을 넣고, 추론 규칙을 생성자로 두면 동적으로 증명을 검사할 수 있음
  • ML의 abstraction barrier 덕분에 부정행위가 불가능하다고 봄
  • 거대한 항이 아무것도 지시하지 않는데도 수십 MB를 차지하는 일은 RAMmageddon 시대에 특히 비합리적으로 다가옴
  • 그런 불필요한 항을 더 우아하게 만드는 연구까지 이어지는 점도 비판함

Isabelle을 고를 이유

  • 동료들이 Lean을 쓰고, 팀의 전문성도 Lean에 있고, 필요한 전제 라이브러리도 Lean에 있다면 Lean을 쓰는 편이 자연스러움
  • 다만 자유롭게 선택할 수 있다면 Isabelle을 검토할 이유는 분명함

  • 자동화

    • 가장 강력한 자동화를 장점으로 들며, 일상적인 “hammer”들과 비교해도 sledgehammer에 견줄 것은 없다고 평가함
    • 컴퓨터 대수 쪽도 별도로 다룰 필요가 있다고 적음

  • 가독성

  • 의존 타입 회피

    • 의존 타입이 없기 때문에 universe level과 초보자를 곤란하게 만드는 여러 특이점을 피할 수 있음
    • Lean의 mathlib와 Rocq의 SSReflect, Mathematical Components에서도 의존 타입 사용은 권장되지 않는다고 적음
    • 의존 타입의 핵심 난점은 제대로 구현하면 타입 검사 자체가 결정 불가능해진다는 점임
    • 이는 동등성 판정이 결정 불가능하기 때문이며, 초기에는 이 점이 당연하게 받아들여졌다고 적음
    • 1990년 무렵부터는 타입 검사를 결정 가능하게 만들기 위해 동등성을 definitional/intensional equality로 낮추는 쪽으로 합의가 이동함
    • 그 결과 (T(N+1))과 (T(1+N))은 서로 다른 타입이 됨
    • 이런 제한은 실제 증명에도 영향을 주며, definitional equality 검사 자체도 여전히 계산 부담이 큼

의존 타입 없이도 가능한 현대 수학

  • 2017년 기준으로는 Isabelle이 어떤 수학까지 감당할 수 있을지 훨씬 더 조심스럽게 봤다고 적음
  • 당시에는 다음 같은 주제를 다루려면 의존 타입이 꼭 필요해 보이기 쉬웠음
  • 그러나 Alexandria 관련 연구를 통해 많은 것을 배웠고, 핵심은 모든 것을 타입으로 밀어 넣지 않는 것이라고 정리함

앞으로의 방향과 AI

  • Lean은 많은 점을 올바르게 잡고 있으며, 중첩된 증명 블록까지 지원해 잠재적으로 충분히 읽기 좋은 증명 언어가 될 수 있음
  • 이제 Lean 공동체가 그런 기능을 실제로 활용해야 하며, Isabelle 사용자들은 이미 대체로 그렇게 하고 있다고 적음
  • 컴퓨터가 검사할 수 있는 증명 객체보다 사람이 실제로 읽을 수 있는 증명 텍스트의 투명성이 더 중요함
  • AI의 부상은 이 차이를 더 선명하게 만듦
  • AI가 만든 증명은 지저분한 경우가 많지만 sledgehammer로 정리하기 쉽고, 구조가 잘 잡혀 있으면 세부가 과해도 읽을 수 있음
  • 그렇게 하면 진행 흐름을 파악하고 더 단순한 형태로 줄이기 쉬워짐
  • 최근에는 언어 모델이 직접 sledgehammer를 호출하는 연구도 나왔음
  • AI는 읽기 쉬운 구조화된 증명을 한 proof assistant에서 다른 proof assistant로 번역하는 일도 쉽게 해낼 수 있음
  • 그렇게 되면 어떤 시스템을 택할지에 대한 부담 자체가 줄어듦

Mizar의 누락 보완

  • 수학 형식화의 역사는 Mizar와 그 방대한 수학 라이브러리 없이 완전해질 수 없음
  • Isabelle의 Isar 언어도 Mizar에서 많은 영향을 받았음
  • Mizar를 빠뜨린 점을 따로 바로잡으며, 다음 글에서 Mizar를 다룰 예정이라고 적음

함께 보면 좋은 글 β

▲
GN⁺ 5시간전  [-]
Hacker News 의견들

  • HN 독자 대부분은 수학자보다 프로그래머에 더 가깝기 때문에, 수학 증명보다 프로그래밍 관점에서 Lean을 보는 편이 더 실용적이라 봄
    함수형 프로그래밍 시각으로 Lean을 다루는 책으로 https://leanprover.github.io/functional_programming_in_lean/가 꽤 좋음
    나도 Lean을 배우는 중이라 초보자의 장밋빛 시각이 좀 있을 수 있지만, 최근 lean-zip 예시처럼 실제 압축/해제 알고리즘 같은 평범한 프로그래머의 코드를 작성하고 증명하는 쪽을 목표로 하고 있음
    https://github.com/kiranandcode/lean-zip/blob/master/Zip/Nat...

    • 이 책을 읽다가 Lean으로 기본적인 컴퓨터 대수 단순화기를 직접 만져봤음
      https://github.com/dharmatech/symbolism.lean
      C# 코드를 옮긴 포팅이고, Lean의 표현력은 놀라울 정도로 큼
    • 그런 용도라면 Dafny도 비슷한 선택지 아닌가 싶음
      예전에 조금 화제가 됐던 걸 봤는데, 이 분야를 최근엔 자세히 따라가진 못했음
    • 1990년대에 소프트웨어 정당성 증명을 실험했던 사례를 기억하는데, 최종 증명 주석 쪽에서 실제 소프트웨어보다 오류가 더 많이 나왔던 걸로 기억함
      그리고 장애물이 두 가지 더 보임. 첫째, 소프트웨어가 무엇을 해야 하는지 아는 것 자체가 어렵고, 사용자가 하고 싶은 일과 고객이 돈을 내는 일이 꼭 같지도 않음
      둘째, 많은 개발자의 작업 품질이 워낙 낮아서 Java 같은 언어보다 진리 언어를 더 잘 다룰 거라고 기대하기 어려움
      다만 두 번째는 필요한 주의를 기울이는 AI 시스템으로 대체되면서 사라질 수도 있어서, 그러면 상황이 바뀔 수 있겠음
    • 비함수형 프로그래밍은 어떠냐는 생각이 듦
      함수형 프로그래밍도 이미 제쳐둔 수학만큼이나 대부분의 프로그래머에게는 큰 관련이 없다고 봄

  • 글쓴이는 Lean을 꽤 잘못 이해한 듯하고, 이 분야를 잘 아는 사람처럼 보여서 더 의외였음
    Lean이 증명 객체를 그대로 보존하고, 최종적으로는 모든 정의가 펼쳐진 거대한 증명 객체 하나를 검사한다고 보는 듯한데, 실제와는 거리가 멂
    Lean은 저자가 LCF의 장점으로 치켜세운 최적화를 사실상 똑같이 구현함. 비유하자면 칠판을 지워가며 증명을 진행하는 방식과 같음
    Lean4에서 def가 아니라 theorem으로 작성하면 그 증명 객체는 더 이상 사용되지 않고, 이건 단순 최적화가 아니라 언어의 핵심 성질임. theorem은 opaque함
    증명 항이 남아 있다 해도 대화형 모드에서 사용자가 볼 수 있게 하려는 용도일 뿐이고, 커널은 그 증명 객체가 무엇이었는지 신경 쓰지도 못함

    • 이건 구현보다 개념적 차이에 더 가까움
      LCF에서는 증명과 항이 다른 것이고, 내 생각엔 원래 그래야 함. 이런 Curry-Howard식 혼동은 불필요한데, 많은 사람이 그게 컴퓨터로 수학을 하는 유일한 방식인 줄 앎
      원하면 LCF에서도 증명을 저장하고 활용할 수 있고, Lean에서도 원하면 최적화로 없앨 수 있을 뿐임
    • 종속 타입 이론에서 증명 객체는 그냥 어떤 타입을 채우는 항 자체인데, 그렇다면 Lean 구현이 그런 항을 만들지 않고도 증명을 구성할 수 있다는 뜻인지 궁금함
    • 맞는 말 같음
      추상 타입 접근이 메모리를 좀 아끼긴 하겠지만 상수배 차이일 뿐이고 점근적 개선은 아님
      Lean이 수십 MB를 낭비한다는 식의 불만은 1980~90년대엔 중요했겠지만, 오늘날엔 그만큼 결정적인 장점은 아닐 수도 있어 보임

  • Lean이 함수형 프로그래밍에 좋다는 말을 많이 듣지만, Agda에서 오면 꽤 투박한 다운그레이드처럼 느껴짐
    tactic도 좋다고 하지만 내 경험상 Coq의 tactic이 더 강력하고 쓰기 편했음
    이게 다 첫인상 편향일 수도 있겠지만, 지금까지는 Lean의 강점이 뭔가 하나를 최고로 잘해서라기보다, 전반적으로 무난하고 커뮤니티가 크다는 데 있는 듯함
    왜 매력적인지는 알겠지만, 그 대가로 아름다움과 힘이 조금 사라진 느낌이라 아쉽기도 함

    • 결국 네트워크 효과라는 얘기이기도 함
      다만 이런 효과는 그 순간에는 영속적처럼 보여도 실제로는 생각보다 오래가지 않음. 정말 그것만 중요했다면 Perl이 지금도 여전히 거물이어야 함
      Lean에선 특히 큰 라이브러리를 먼저 확보한 점이 큼. Perl에게 CPAN이 그랬던 것과 비슷함
      하지만 스케일링 법칙을 보면 대부분의 사용자에게 큰 라이브러리의 가치는 크기의 로그 정도로 늘어날 가능성이 큼
      https://pdodds.w3.uvm.edu/teaching/courses/2009-08UVM-300/do...
      초반엔 이 격차가 넘을 수 없어 보이지만, 꼭 규모를 따라잡지 않아도 어느 순간부터는 사용성이 더 중요해짐
      게다가 수학 라이브러리 포팅은 LLM에 잘 맞는 작업이기도 함. 소스는 검증돼 있고, 타깃도 검증 가능하며, 추론 경로도 대체로 옮길 수 있음
      반대로 말하면 LLM 덕분에 소수 플랫폼에서 일하는 장벽도 예상보다 낮아짐. 그쪽 라이브러리를 내 플랫폼으로 옮길 수 있다면, 내 증명도 그쪽으로 옮길 수 있을 가능성이 큼
    • 오히려 그건 커뮤니티가 마침내 성숙해서 실제 작업을 하기 시작했다는 뜻처럼 보임
      완벽한 도구가 핵심은 아니고, 충분히 좋은 도구로 일을 해내는 게 더 중요함
    • Agda는 증명 검사기로는 더 좋지만, 소프트웨어를 만드는 실용적 선택지는 아니라고 봄
      Lean은 진짜로 Haskell의 후계자가 될 수도 있을 만큼, 소프트웨어 개발용 함수형 언어로 성장할 여지가 있어 보임
    • Agda는 조금, Lean은 그보다 더 써봤는데, 수학 증명보다 일반 함수형 프로그램을 쓰는 건 Lean이 훨씬 쉬웠음
      차이는 주로 도구 지원에서 났던 것 같음. Agda 문서는 부실하고 시스템에 설치해서 굴리는 것도 번거롭고, 사실상 Emacs를 쓰길 강하게 요구함
      반면 Lean은 자체 문서에 cat 유틸리티 작성법까지 있고, 전반적으로 훨씬 현대적인 tooling 경험을 줌
    • Agda의 함수형 프로그래밍에서 정확히 어떤 점이 좋은지 궁금함
      보통 칭찬은 dependent pattern matching 쪽에서 많이 듣는데, 그 부분에서는 Lean이 꽤 약하다고 느낌
      그래도 일반적인 FP에서도 Agda가 더 친화적이라고 느낀다면, 어떤 점에서 그런지 듣고 싶음

  • Isabelle/HOL은 언어 자체는 괜찮지만, 툴링에는 데스크톱 중심 접근을 떠나서도 깊은 결함이 있음
    언어는 Lean과 다르지 꼭 더 낫다는 건 아니고, 종속 타입에 대한 몇몇 비판에는 동의함
    결국 두 언어는 서로 다른 트레이드오프를 했고, 그 선택이 각자 영역에서 꽤 효율적인 도구가 되게 만든 듯함. 증명이라는 영역 자체가 넓어서 패러다임마다 강약점이 다르고, Lean은 그중 다른 부분에 특화됐을 뿐임
    Sledgehammer는 좋지만, Lean에도 비슷한 것이 생기는 건 시간문제 같음
    탐색 단계에서는 유용할 수 있어도 리소스를 많이 먹고, 증명을 짧게 만들긴 하지만 공개된 코드에서는 반쯤 마법 같은 by sledgehammer보다 증명의 전체 단계가 직접 드러나는 편을 더 선호함
    반면 Isabelle 자체를 개발하는 일은 Lean보다 훨씬 고통스럽고, 특히 개발자들과 소통하는 과정이 그럼
    메일링 리스트에서 버그는 없고 예상 못 한 동작만 있다는 식의 태도는 유치하고 비전문적으로 보였음
    그리고 Lean과 비슷한 시스템의 RAM 사용량을 비꼬는 것도, Isabelle 쪽의 메모리 폭식을 보면 꽤 우스운 얘기임

    • 여기서 문제는 UNSAT 인증서를 빠르게 검사 가능한 형태로 만드는 일이 전혀 사소하지 않다는 데 있음
      사실상 그 자체가 형식 증명을 쓰는 것과 비슷한 난이도임
    • 마지막으로 확인했을 때 Isabelle/HOL은 커스텀 Emacs 모드를 인터페이스로 썼던 걸로 기억함
      다른 HOL과 헷갈린 걸 수도 있음
    • Sledgehammer가 뭔지는 모르지만, 설명만 보면 Mathlib의 grind와 거의 같은 도구처럼 들림
      https://leanprover-community.github.io/mathlib4_docs/Init/Gr...

  • Lean에서 흥미로운 건 Lean은 언어인데, 사람들이 주로 이야기하는 건 사실 Mathlib이라는 라이브러리라는 점임
    Mathlib 제작자들은 꽤 실용주의적으로 보이고, 그래서 Lean 타입 안에 고전 논리를 넣고 직관주의 논리는 일부만 쓰는 듯함

    • 배중률을 설명하면서 든 예시는 틀렸음
      "어떤 것이 동시에 참이고 거짓일 수 없다"는 건 배중률이 아니라 모순율임
      배중률은 p가 참이거나 not p가 참이라는 뜻임
      https://en.wikipedia.org/wiki/Law_of_noncontradiction
    • 컴퓨터과학 쪽은 이제 자기들만의 CSLib를 만들고 있음
      https://www.cslib.io https://www.github.com/leanprover/cslib
      직관주의 논리는 본질적으로 계산 가능한 구성물로 수학적 논증을 바꾸려는 데 의미가 있으니, 이 문제를 어떻게 다룰지 흥미로움
      사실 Lean으로 알고리즘을 쓰는 순간 이미 어떤 형태로든 구성적인 제약 안에 들어가고, 그 목적엔 그 정도 논리만으로 충분할 수도 있음
    • 구성주의 수학을 받아들이는 5단계라는 농담이 떠오름
      부정, 분노, 타협, 우울, 수용
      Andrej Bauer의 관련 강연과 글도 참고할 만함
      https://www.youtube.com/watch?v=21qPOReu4FI
      http://dx.doi.org/10.1090/bull/1556
    • 여기서 말한 건 intuitive logic이 아니라 intuitionistic logic이어야 함
    • 그런 제약과 막힘이 많은데도, 언제 왜 직관주의 논리를 선호하게 되는지 궁금함

  • 이런 글은 더 많이 필요하다고 봄
    모두가 당연하다는 듯 그냥 X를 써라라고 밀어붙이는 집단사고에 대해서도, 적어도 대안을 검토할 만한 설득력 있는 이유는 늘 있음
    결국 대안을 버리고 주류를 택하더라도, 지형을 알고 선택하는 편이 더 낫다고 봄

    • 완전히 동의하지 않음
      지금도 프레임워크와 대안을 너무 많이 만들고 있고, 아마 재미있어서 더 그런 듯함
      기존 도구를 개선하거나 그냥 실제 일을 진행하는 대신, 언어와 라이브러리와 빌드 도구를 끝없이 늘리는 쪽으로 가는 경우가 많음
      언어도 라이브러리도 빌드 툴도 지금의 절반만 있었으면 오히려 더 나았을 거라 봄
    • 결국 상황에 따라 다름
      주류에서 벗어날수록 문서는 줄고, 덜 탐색된 구석 때문에 버그는 늘고, 도움받을 사람도 적어짐
      선택지가 스무 개 넘게 쌓이면 평균적으로는 표준 선택지를 고르고 넘어가는 게 맞음. 주의력은 유한해서, 의존성마다 조사 보고서를 쓰다 보면 정작 핵심 문제를 못 풂
      예외는 두 가지인데, 표준 도구가 내 사용 사례에 실제로 맞지 않거나, 표준 도구 자체가 내가 풀려는 핵심 문제와 크게 겹칠 때임

  • 이런 논의는 Python의 과학 컴퓨팅 한계를 지적하는 글들과 비슷하게 느껴짐
    어느 정도 괜찮은 도구 주위에 커뮤니티가 임계질량을 넘겨 모이면, 그게 다른 대부분의 요소를 압도함
    모멘텀이 붙고, 튜토리얼과 설명 글과 더 나은 문서가 쌓이면서 사실상 탈출 속도에 도달함
    Lean은 Terrance Tao 같은 강력한 지지자까지 있어서 지금 딱 그런 위치에 있는 듯함
    그래서 "언어 X가 더 낫다"는 말이 완전히 틀린 건 아니어도, 정작 중요한 질문은 놓치기 쉬움
    모두가 알고 있고 바로 쓸 수 있고 더 많은 시간이 개선에 투입되는 그 도구보다 실제로 더 나은가가 핵심임
    결국 worse is better, 혹은 좋고 인기 있으면 그 정도로 충분하다는 상황처럼 보임

    • LLM이 서로 다른 형식 체계 번역을 꽤 효과적으로 가능하게 해줄 거라는 점은 좋은 포인트라고 봄
      특히 이 분야는 번역 결과를 상당 부분 자동 검증할 수 있어서, 선택 자체가 그리 큰 문제는 아닐 수 있음
    • 하지만 AI 시대에는 임계질량의 중요성이 훨씬 덜함
      AI는 거대한 커뮤니티 라이브러리가 없어도 스스로 코드를 작성할 수 있고, 인터넷에 튜토리얼이 백만 개 떠다니지 않아도 문서와 스펙을 직접 읽음
      잡시장이 없는 언어를 피할 필요도 없음. AI는 경력을 쌓는 게 아니라 지금 맡은 일을 하면 되기 때문임
      그래서 예전 같으면 기회가 없었을 소형 언어와 DSL도 채택될 여지가 커짐
      프로그래밍에서 오래 지속된 언어 단일문화도 AI가 끝낼 수 있다고 봄

  • "오늘날 어떤 시스템으로 형식화된 거의 모든 것은 AUTOMATH로도 형식화할 수 있었을 것"이라는 말은, 오늘날 현대 언어로 짜는 건 50년 전 어셈블리로도 다 짤 수 있었다고 말하는 것과 비슷함
    기술적으로는 맞아도 경제적으로는 전혀 다름

    • 어셈블리 언어는 대체로 튜링 완전한데, 증명 엔진 쪽에서 그에 대응하는 비교가 정확히 뭔지는 잘 모르겠음

  • 15년쯤 전에 Coq/Rocq와 몇몇 다른 도구를 만져보려 했는데, 개념보다도 소프트웨어 자체를 도통 이해하기 어려웠음
    증명 보조기/대화형 정리증명기에서 이상한 점은, interactive라는 성격 때문에 언어와 IDE가 결합된 형태가 되고 실제로도 둘이 강하게 엮인다는 데 있음
    그래서 언어만 따로 떼어 말하기가 어렵고, 어떤 환경에서 쓰는지도 같이 봐야 함
    나도 VS Code의 열렬한 팬은 아니지만, 수많은 사람이 쓰고 큰돈이 들어가며 다듬어진 확장 가능한 IDE가 대안들의 환경보다 훨씬 앞서 있다는 건 분명함
    Natural Numbers Game 같은 훌륭한 입문 경로도 VS Code의 해킹 가능성과 생태계 덕분에 가능한 것처럼 보임
    다만 Lean을 배우며 걱정되는 건 문법 확장성이 양날의 검이라는 점임
    언어를 익힌 뒤에는 그 언어로 쓴 코드를 읽고 싶어지는데, 프로젝트마다 자기 DSL을 잔뜩 만들기 시작하면 통제가 안 될 수 있음
    결국 이건 커뮤니티와 생태계가 얼마나 절제하느냐에 달렸고, 그래서 좀 기대 반 걱정 반으로 보고 있음

  • Lean은 수학자들에게 가장 사랑받는 증명 보조기도 아니고, 소프트웨어 형식 검증에 가장 잘 맞는 도구도 아님
    다만 둘 다 그럭저럭 해내고, 대신 가장 얻기 어려운 모멘텀을 잡았음
    게다가 AI 시대에는 공개된 인간 작성 코드의 양이 에이전트가 새 코드를 얼마나 잘 만들어내는지에 직접 영향을 주기 때문에, 그 모멘텀이 더 강해짐

답변달기