그런 용도라면 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과 헷갈린 걸 수도 있음
컴퓨터과학 쪽은 이제 자기들만의 CSLib를 만들고 있음 https://www.cslib.iohttps://www.github.com/leanprover/cslib
직관주의 논리는 본질적으로 계산 가능한 구성물로 수학적 논증을 바꾸려는 데 의미가 있으니, 이 문제를 어떻게 다룰지 흥미로움
사실 Lean으로 알고리즘을 쓰는 순간 이미 어떤 형태로든 구성적인 제약 안에 들어가고, 그 목적엔 그 정도 논리만으로 충분할 수도 있음
여기서 말한 건 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 시대에는 공개된 인간 작성 코드의 양이 에이전트가 새 코드를 얼마나 잘 만들어내는지에 직접 영향을 주기 때문에, 그 모멘텀이 더 강해짐
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...
https://github.com/dharmatech/symbolism.lean
C# 코드를 옮긴 포팅이고, Lean의 표현력은 놀라울 정도로 큼
예전에 조금 화제가 됐던 걸 봤는데, 이 분야를 최근엔 자세히 따라가진 못했음
그리고 장애물이 두 가지 더 보임. 첫째, 소프트웨어가 무엇을 해야 하는지 아는 것 자체가 어렵고, 사용자가 하고 싶은 일과 고객이 돈을 내는 일이 꼭 같지도 않음
둘째, 많은 개발자의 작업 품질이 워낙 낮아서 Java 같은 언어보다 진리 언어를 더 잘 다룰 거라고 기대하기 어려움
다만 두 번째는 필요한 주의를 기울이는 AI 시스템으로 대체되면서 사라질 수도 있어서, 그러면 상황이 바뀔 수 있겠음
함수형 프로그래밍도 이미 제쳐둔 수학만큼이나 대부분의 프로그래머에게는 큰 관련이 없다고 봄
글쓴이는 Lean을 꽤 잘못 이해한 듯하고, 이 분야를 잘 아는 사람처럼 보여서 더 의외였음
Lean이 증명 객체를 그대로 보존하고, 최종적으로는 모든 정의가 펼쳐진 거대한 증명 객체 하나를 검사한다고 보는 듯한데, 실제와는 거리가 멂
Lean은 저자가 LCF의 장점으로 치켜세운 최적화를 사실상 똑같이 구현함. 비유하자면 칠판을 지워가며 증명을 진행하는 방식과 같음
Lean4에서
def가 아니라theorem으로 작성하면 그 증명 객체는 더 이상 사용되지 않고, 이건 단순 최적화가 아니라 언어의 핵심 성질임. theorem은 opaque함증명 항이 남아 있다 해도 대화형 모드에서 사용자가 볼 수 있게 하려는 용도일 뿐이고, 커널은 그 증명 객체가 무엇이었는지 신경 쓰지도 못함
LCF에서는 증명과 항이 다른 것이고, 내 생각엔 원래 그래야 함. 이런 Curry-Howard식 혼동은 불필요한데, 많은 사람이 그게 컴퓨터로 수학을 하는 유일한 방식인 줄 앎
원하면 LCF에서도 증명을 저장하고 활용할 수 있고, 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 덕분에 소수 플랫폼에서 일하는 장벽도 예상보다 낮아짐. 그쪽 라이브러리를 내 플랫폼으로 옮길 수 있다면, 내 증명도 그쪽으로 옮길 수 있을 가능성이 큼
완벽한 도구가 핵심은 아니고, 충분히 좋은 도구로 일을 해내는 게 더 중요함
Lean은 진짜로 Haskell의 후계자가 될 수도 있을 만큼, 소프트웨어 개발용 함수형 언어로 성장할 여지가 있어 보임
차이는 주로 도구 지원에서 났던 것 같음. Agda 문서는 부실하고 시스템에 설치해서 굴리는 것도 번거롭고, 사실상 Emacs를 쓰길 강하게 요구함
반면 Lean은 자체 문서에
cat유틸리티 작성법까지 있고, 전반적으로 훨씬 현대적인 tooling 경험을 줌보통 칭찬은 dependent pattern matching 쪽에서 많이 듣는데, 그 부분에서는 Lean이 꽤 약하다고 느낌
그래도 일반적인 FP에서도 Agda가 더 친화적이라고 느낀다면, 어떤 점에서 그런지 듣고 싶음
Isabelle/HOL은 언어 자체는 괜찮지만, 툴링에는 데스크톱 중심 접근을 떠나서도 깊은 결함이 있음
언어는 Lean과 다르지 꼭 더 낫다는 건 아니고, 종속 타입에 대한 몇몇 비판에는 동의함
결국 두 언어는 서로 다른 트레이드오프를 했고, 그 선택이 각자 영역에서 꽤 효율적인 도구가 되게 만든 듯함. 증명이라는 영역 자체가 넓어서 패러다임마다 강약점이 다르고, Lean은 그중 다른 부분에 특화됐을 뿐임
Sledgehammer는 좋지만, Lean에도 비슷한 것이 생기는 건 시간문제 같음
탐색 단계에서는 유용할 수 있어도 리소스를 많이 먹고, 증명을 짧게 만들긴 하지만 공개된 코드에서는 반쯤 마법 같은
by sledgehammer보다 증명의 전체 단계가 직접 드러나는 편을 더 선호함반면 Isabelle 자체를 개발하는 일은 Lean보다 훨씬 고통스럽고, 특히 개발자들과 소통하는 과정이 그럼
메일링 리스트에서 버그는 없고 예상 못 한 동작만 있다는 식의 태도는 유치하고 비전문적으로 보였음
그리고 Lean과 비슷한 시스템의 RAM 사용량을 비꼬는 것도, Isabelle 쪽의 메모리 폭식을 보면 꽤 우스운 얘기임
사실상 그 자체가 형식 증명을 쓰는 것과 비슷한 난이도임
다른 HOL과 헷갈린 걸 수도 있음
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
https://www.cslib.io https://www.github.com/leanprover/cslib
직관주의 논리는 본질적으로 계산 가능한 구성물로 수학적 논증을 바꾸려는 데 의미가 있으니, 이 문제를 어떻게 다룰지 흥미로움
사실 Lean으로 알고리즘을 쓰는 순간 이미 어떤 형태로든 구성적인 제약 안에 들어가고, 그 목적엔 그 정도 논리만으로 충분할 수도 있음
부정, 분노, 타협, 우울, 수용
Andrej Bauer의 관련 강연과 글도 참고할 만함
https://www.youtube.com/watch?v=21qPOReu4FI
http://dx.doi.org/10.1090/bull/1556
이런 글은 더 많이 필요하다고 봄
모두가 당연하다는 듯 그냥 X를 써라라고 밀어붙이는 집단사고에 대해서도, 적어도 대안을 검토할 만한 설득력 있는 이유는 늘 있음
결국 대안을 버리고 주류를 택하더라도, 지형을 알고 선택하는 편이 더 낫다고 봄
지금도 프레임워크와 대안을 너무 많이 만들고 있고, 아마 재미있어서 더 그런 듯함
기존 도구를 개선하거나 그냥 실제 일을 진행하는 대신, 언어와 라이브러리와 빌드 도구를 끝없이 늘리는 쪽으로 가는 경우가 많음
언어도 라이브러리도 빌드 툴도 지금의 절반만 있었으면 오히려 더 나았을 거라 봄
주류에서 벗어날수록 문서는 줄고, 덜 탐색된 구석 때문에 버그는 늘고, 도움받을 사람도 적어짐
선택지가 스무 개 넘게 쌓이면 평균적으로는 표준 선택지를 고르고 넘어가는 게 맞음. 주의력은 유한해서, 의존성마다 조사 보고서를 쓰다 보면 정작 핵심 문제를 못 풂
예외는 두 가지인데, 표준 도구가 내 사용 사례에 실제로 맞지 않거나, 표준 도구 자체가 내가 풀려는 핵심 문제와 크게 겹칠 때임
이런 논의는 Python의 과학 컴퓨팅 한계를 지적하는 글들과 비슷하게 느껴짐
어느 정도 괜찮은 도구 주위에 커뮤니티가 임계질량을 넘겨 모이면, 그게 다른 대부분의 요소를 압도함
모멘텀이 붙고, 튜토리얼과 설명 글과 더 나은 문서가 쌓이면서 사실상 탈출 속도에 도달함
Lean은 Terrance Tao 같은 강력한 지지자까지 있어서 지금 딱 그런 위치에 있는 듯함
그래서 "언어 X가 더 낫다"는 말이 완전히 틀린 건 아니어도, 정작 중요한 질문은 놓치기 쉬움
모두가 알고 있고 바로 쓸 수 있고 더 많은 시간이 개선에 투입되는 그 도구보다 실제로 더 나은가가 핵심임
결국 worse is better, 혹은 좋고 인기 있으면 그 정도로 충분하다는 상황처럼 보임
특히 이 분야는 번역 결과를 상당 부분 자동 검증할 수 있어서, 선택 자체가 그리 큰 문제는 아닐 수 있음
AI는 거대한 커뮤니티 라이브러리가 없어도 스스로 코드를 작성할 수 있고, 인터넷에 튜토리얼이 백만 개 떠다니지 않아도 문서와 스펙을 직접 읽음
잡시장이 없는 언어를 피할 필요도 없음. AI는 경력을 쌓는 게 아니라 지금 맡은 일을 하면 되기 때문임
그래서 예전 같으면 기회가 없었을 소형 언어와 DSL도 채택될 여지가 커짐
프로그래밍에서 오래 지속된 언어 단일문화도 AI가 끝낼 수 있다고 봄
"오늘날 어떤 시스템으로 형식화된 거의 모든 것은 AUTOMATH로도 형식화할 수 있었을 것"이라는 말은, 오늘날 현대 언어로 짜는 건 50년 전 어셈블리로도 다 짤 수 있었다고 말하는 것과 비슷함
기술적으로는 맞아도 경제적으로는 전혀 다름
15년쯤 전에 Coq/Rocq와 몇몇 다른 도구를 만져보려 했는데, 개념보다도 소프트웨어 자체를 도통 이해하기 어려웠음
증명 보조기/대화형 정리증명기에서 이상한 점은, interactive라는 성격 때문에 언어와 IDE가 결합된 형태가 되고 실제로도 둘이 강하게 엮인다는 데 있음
그래서 언어만 따로 떼어 말하기가 어렵고, 어떤 환경에서 쓰는지도 같이 봐야 함
나도 VS Code의 열렬한 팬은 아니지만, 수많은 사람이 쓰고 큰돈이 들어가며 다듬어진 확장 가능한 IDE가 대안들의 환경보다 훨씬 앞서 있다는 건 분명함
Natural Numbers Game 같은 훌륭한 입문 경로도 VS Code의 해킹 가능성과 생태계 덕분에 가능한 것처럼 보임
다만 Lean을 배우며 걱정되는 건 문법 확장성이 양날의 검이라는 점임
언어를 익힌 뒤에는 그 언어로 쓴 코드를 읽고 싶어지는데, 프로젝트마다 자기 DSL을 잔뜩 만들기 시작하면 통제가 안 될 수 있음
결국 이건 커뮤니티와 생태계가 얼마나 절제하느냐에 달렸고, 그래서 좀 기대 반 걱정 반으로 보고 있음
Lean은 수학자들에게 가장 사랑받는 증명 보조기도 아니고, 소프트웨어 형식 검증에 가장 잘 맞는 도구도 아님
다만 둘 다 그럭저럭 해내고, 대신 가장 얻기 어려운 모멘텀을 잡았음
게다가 AI 시대에는 공개된 인간 작성 코드의 양이 에이전트가 새 코드를 얼마나 잘 만들어내는지에 직접 영향을 주기 때문에, 그 모멘텀이 더 강해짐