아, 저도 지난해 여름부터 둠 이맥스를 쓰고 있어요. 수학 기초론 밖의 수학 분야를 연구하는 수학자들이 현재 가장 활발히 이용하고 있는 증명 보조기가 린이라고 생각해서 저는 린을 골랐습니다. 현재로서는 사람들이 린을 이용할 가장 큰 동기가 린의 수학 라이브러리인 매스리브(Mathlib)뿐인 듯해요.
인공 지능의 대답을 검토해 보자면, 린은 구문이 깔끔한 편이고 커뮤니티가 활발하지만, 자동화 도구와 공식 문서가 아직은 부족합니다. 이 두 가지는 앞으로 개선될 여지가 있어요.
그런데 제가 요즘 린 핵심[코어] 개발진에 대한 불만이 쌓이고 있기 때문에, 린보다는 그 밖의 증명 보조기 중 하나를 더 자주 이용할 계획입니다.
제 불만은 다음과 같습니다. 린 핵심 개발진이 린의 개발 방향을 확정하기 전에 린 커뮤니티에 속한 다른 인원들이 자신의 의견을 핵심 개발진에게 전달할 방법이 없습니다. 따라서 린의 개발에 관한 논의는 린 핵심 개발진 내부에서만 일어납니다. 개발진 외부에서 일어나는 것은 논의가 아니라 반응입니다. 핵심 개발진은 이미 결정을 다 내린 상태에서 그 결정을 린 커뮤니티에 통보할 뿐이고, 그 통보도 그리 자세하거나 빠르지 않습니다.
Mario Carneiro said:
I was indeed notified that some tactics were going to move, not really in a way which invited discussion but more of a "heads up this is happening". I have to admit that the scale turned out to be much bigger than I expected and now there isn't much left within the original purview of Std from what I can tell. Most of the things on Joe's original Std roadmap are now in an uncertain position and I don't know what will remain. Perhaps future announcements will clarify matters here, but I certainly haven't gotten the impression that I have any say over the contents of those announcements.
위의 인용문에서 언급된 일은 올해 4월쯤에 있었습니다. 다음 인용문은 어제 제가 통보받은 내용에 대한 제 반응입니다.
Bulhwi Cha said:
Kim Morrison said:
There will be more news coming about this later, and when a design document is available we will post it, but it is possible there will be a radical overhaul of the
Stringlibrary (indeed, even the definition ofString), so I would hesitate to encourage significant work onStringat the moment as it may become obsolete (even to the point of not being able to meaningfully migrate results).I'm glad that there may be a substantial overhaul of definitions and theorems about strings in the future. But it also means that I don't have to prove the ten specification theorems and review Batteries#809.
지난 4월에 제가 서강올빼미에 게시한 글 '어떤 오류가 사소한 실수인가'에서도 밝혔다시피, 문자열 연산 String.splitOn의 명세에 관한 정리 String.splitOn_of_valid를 제가 증명하는 데 170시간 정도가 걸렸습니다. 이 증명을 린 배터리(Batteries, 옛 표준 라이브러리) 관리자가 검토하기를 제가 두 달 동안 기다리고 있었는데, 린 핵심 개발진이 문자열에 관한 라이브러리를 미래에 대폭 수정할 수 있다는 소식을 어제 제게 알렸습니다.
현재 몇몇 문자열 연산은 그에 관한 정리를 작성하기가 어렵게 정의돼 있다고 제가 이전에 린 줄립 챗에서 밝힌 바 있기 때문에 저도 이 변화를 환영합니다. 하지만 이제 제가 고생해서 작성한 증명은 검토받지도 못하게 됐어요. 문자열 연산의 정의가 크게 바뀔수록 그에 관한 정리의 증명도 크게 바뀔 수 있기 때문입니다.
제 증명이 쓸모없어질 가능성이 꽤 커졌다는 사실은 저도 받아들일 수 있어요. 하지만 문자열에 관한 라이브러리를 대규모로 재정비할지를 린 핵심 개발진이 논의했을 동안 저는 그 논의에 참여할 수 없었다는 점이 불만스럽습니다. 그분들이 어떤 결정을 내리기 전에 일반 린 이용자들의 의견을 들어 보기만 해도 좋았을 것입니다.
공개 소스 소프트웨어의 관리자가 어떤 결정을 내리기 전에 이용자의 의견을 듣지 않아도 되기는 합니다. 관리자는 자신이 원하는 대로 소프트웨어를 개발할 수 있어요. 그 대신에 이용자는 그 소프트웨어의 대용품을 찾든가 그것을 분할[포크]해서 자신만의 버전을 개발할 수 있습니다.
제가 매스리브를 참고해 수학을 형식화하고 싶기 때문에 린을 그만 이용할 수는 없지만, 앞으로는 메타매스 제로(논문 링크) 검증 시스템과 다프니(Dafny) 프로그래밍 언어를 다루는 데 시간을 더 들이려고 합니다.