소프트웨어의 추상적 정확성과 현실 작동은 분리되며, 시스템 설계 단계부터 근본적인 재설계가 필요합니다. 본문은 형식 검증의 중요성을 강조하며, LLM이 가진 토큰 기반 기호 추론의 한계를 지적합니다. 따라서 합리적인 시간 안에 정확한 소프트웨어를 작성하려면 분석하기 쉬운 언어와 코딩 방식 사용이 필수적입니다.
AI 자동 생성 콘텐츠
본 콘텐츠는 GeekNews의 원문을 AI가 자동으로 요약·번역·분석한 것입니다. 원 저작권은 원저작자에게 있으며, 정확한 내용은 반드시 원문을 확인해 주세요.
원문 바로가기소프트웨어의 추상적·수학적 정확성과 현실에서의 작동은 분명히 구분된다고 봄. 입력을 처리하고 사람에게 복잡한 작업 흐름을 제공하는 소프트웨어라면 현실의 끝없는 변수를 피할 수 없음.
형식적 정확성도 가치가 있지만, 언제 유용하고 언제 비용이 효용보다 커지는지 구분하는 것이 핵심임.
해결하려는 대상 자체가 반드시 모호하다기보다, 현대 소프트웨어가 애초에 형식적 수학 모델과 멀어지는 방향으로 발전한 탓에 가까워 보임. 운영체제와 개발의 기본 요소부터 그런 방향으로 설계되어 있음.
파일 시스템을 다루는 프로그램의 명세를 형식화하기 어려운 큰 이유는 파일 시스템이 모든 실행 프로그램의 공유 객체이기 때문임. 컨테이너화, 네임스페이스, pledge 등으로 달라지고는 있지만, 프로그램이 올바른 자격 증명으로 시스템 호출을 하면 언제든 루트 권한을 얻을 수 있다는 점까지 더해져 가능한 상태를 배제하기가 매우 어려워짐.
다르게 만들 수도 있지만, 시스템과 문제를 바라보는 방식부터 근본적으로 재설계해야 함.
높은 신뢰도의 소프트웨어를 만들 수 있어야 함. 고객을 완전히 속인 게 아니라면 제품이 목적에 맞고, 실제로 사용하기에 적합하며, 안전하리라고 기대하는 것이 당연함.
정확성까지 증명된 상용 소프트웨어가 드물고 증명이 어렵다는 것은 알고 있음. 하지만 앞의 세 가지 중 하나만 충족하는 것조차 버거워 보이며, 바로 여기에 전문가다운 엄밀함과 성실함이 필요함.
둘은 구분되지만, 정확성은 토대라는 점을 놓치고 있음. 정확하다는 것만으로 충분하지는 않지만, 프로그램이 정확하지조차 않다면 의도대로 작동할 가능성도 사실상 없음.
대부분의 소프트웨어에서 검증의 필요성이 상대적으로 낮았던 것은 맞지만, 군사·의료·산업 자동화 소프트웨어에는 언제나 추상적·수학적 정확성이 필요했음.
글이 쓰일 당시에는 이런 분야가 주된 배경이었겠지만, AI와 LLM이 대규모로 배포되는 지금도 잘 들어맞는다고 봄. 정확한 소프트웨어를 작성할 때 토큰 기반 시스템과 LLM 내부의 기호 추론이 지니는 근본적 한계를 보여주기 때문임.
인간에게도 같은 한계가 적용되지만, 인간의 정신적 모델링은 전적으로 기호 처리에 의존하지 않으며 실제로 정확한 소프트웨어를 만들어 왔음. 반면 AI와 LLM은 그런 능력이 입증되지 않았고, 이 글에 비춰 보면 현재의 토큰 기반 기술로는 앞으로도 어려울 듯함.
부정적 명제에서 가장 중요한 것은 어떤 합리적 가정을 추가하면 결론이 달라지는가임.
라이스 정리에 따르면 임의의 함수가 항상 두 입력의 합을 계산하는지 판정하는 프로그램은 만들 수 없음. 하지만 이는 분석이 임의로 어려운 구현까지 허용하기 때문이며, 단순한 덧셈 구현의 정확성을 증명할 수 있다는 사실과 모순되지 않음.
따라서 가장 적절한 결론은 “합리적인 시간 안에 정확한 소프트웨어를 작성하려면 분석하기 쉬운 언어와 코딩 방식을 사용해야 한다”라고 봄.
먼저 정확하다는 것의 의미부터 정해야 함. 형식 명세를 만족한다는 뜻인가? 그렇다면 그 명세가 정확하다는 것은 어떻게 아는가? 정의상 정확하다고 간주하는 것인가?
글은 라이스 정리를 Yedidiya와 Aaronson이 만든 작은 프로그램에 관해서는 아무것도 증명할 수 없다는 뜻과 혼동하는 듯함. 하지만 정리는 모든 프로그램에 대해 특정 지점에 도달하는지를 항상 올바르게 판정하는 일반적 방법을 만들 수 없다는 뜻임.
특정 프로그램을 개별적으로 증명할 때는 많은 것을 증명할 수 있음. 또는 루프가 종료한다고 가정하는 식으로 과대근사를 적용하면, 실제로는 올바른 일부 프로그램을 거부할 위험을 감수하면서도 많은 속성을 건전하게 증명할 수 있음. 타입 시스템이 그런 예임.
다만 글의 표현이나 내 해석에서 생긴 차이일 수도 있음.
형식 검증에 늘 관심이 있었지만, 직접 해본 것은 작은 연습용 증명과 증명에서 프로그램을 도출하는 작업 정도임.
“AI가 Lean을 한다”거나 형식 검증이 쉽고 AI에게는 더 쉬워질 테니 사람이 머리를 쓸 필요가 없다는 가정에서 벗어난 예전 논의를 보니 반가움.
애초에 검증 가능한 프로그램을 설계하는 일부터 깊은 사고와 문제에 대한 통찰을 요구하는 어려운 작업임.
BB(6), 즉 기호 2개·상태 6개인 바쁜 비버의 최고 기록 하한을 보면 글이 쓰인 시기가 드러나 흥미로움. 글에는 >10^36534로 나오지만, 현재 최고 기록인 mxdys 2025는 >10↑↑10↑↑10↑↑8임. 10↑↑8은 10을 높이 8로 쌓은 거듭제곱 탑이고, 전체 식은 오른쪽부터 계산하므로 10↑↑10↑↑8만 해도 이미 상상을 초월하는 크기임.
진짜 질문은 증명할 수 없는 프로그램이 존재하더라도 일반적인 프로그램은 증명할 수 있는가임. 글에 나온 예제보다 내가 쓰는 워드프로세서나 웹 브라우저가 관심사임. 스크립트 언어에 제약을 두면 이런 프로그램을 증명할 수 있을까?
이것만으로 전부 해결되지는 않지만, 신뢰할 수 있는 코드를 만드는 수단으로 순수 함수보다 나은 것은 아직 보지 못했음.
내가 작성한 코드에는 CORS를 다루거나 환경 변수를 읽거나 .ssh 디렉터리를 살펴보게 할 수 있지만, 가져온 모듈까지 그런 일을 할 수 있기를 바라지는 않음.
정확성 증명까지 고려하지 않더라도 스크립트 언어에 제약을 두는 일은 그리 어렵지 않을 것임. 명세에 악의적인 행위자가 제약을 우회할 만한 허점이 없어 보이고, 올바르게 구현하면 제약이 실제로 지켜질 가능성이 매우 높다면, 노력을 들여 검증된 구현을 작성하는 것도 가능하리라 봄.
하지만 사람들이 원하는 방향은 다름. 예컨대 HTML5 이후 WHATWG의 웹 표준 발전은 사실상 모두 JavaScript로 할 수 있는 일을 확장하는 쪽이었음.
형식 검증은 돌로 작업하는 것과 비슷함. 원하는 형태를 이미 안다면 견고하고 오래가는 구조물을 만들 수 있지만, 이것저것 시도하는 단계라면 스케치하거나 부드러운 점토를 쓰는 편이 나음.
Rust처럼 그보다 덜 엄격한 언어에도 같은 불만이 있음. 아이디어를 탐색할 뿐인데도 실서비스 수준의 코드를 요구하기 때문임. 정확성보다 감각과 반복 개발 속도가 중요한 게임과 웹사이트에는 그래서 부적합하다고 봄. 버그가 없으면 좋겠지만, 유연성과 개발 속도를 높이는 편이 대체로 더 가치 있음.
스타트업이나 독립 개발자는 버틸 수 있는 기간이 짧음. 메모리 누수를 없애겠다고 그 기간을 절반으로 줄이면 수만~수십만 달러가 들거나 출시와 실패를 가를 수도 있음.
Python처럼 허술하지만 온갖 기호 처리를 유연하게 허용하는 언어가 없었다면 오늘날의 AI도 없었을 것임. 연구자들이 메모리나 프로세서 배치를 신경 쓰지 않고 몇 줄을 바로 실행할 수 있었기에 프로그램 자체를 만들 수 있었음. CUDA와 torch의 계산 그래프 “컴파일”로 보완하고 있지만, 성능을 겨우 맞추기 위해 엄청난 노력을 들인 JS와 Python 위에서 대부분의 소프트웨어가 돌아가는 현실은 아름다운 재앙 같음.
소프트웨어의 실상을 온전히 보는 것은 개발자뿐임. 나머지는 추상화만 보며, 흉측한 장치를 덮어 둔 천을 보는 셈임. 대중은 그 천의 겉모습조차 감당하기 어려워함.
경영진과 마케팅 부서는 그 천에 대한 제삼자의 막연한 설명 정도만 감당할 수 있음.
하드웨어 엔지니어도 똑같이 말함. 컴퓨터의 실상을 온전히 보는 것은 자신들뿐이며, 소프트웨어 엔지니어는 흉측한 현실을 가려 주는 추상화만 본다는 것임.
내 머리가 Goldbach의 100분의 1 수준일지라도 동의하기 어려움. 실제 프로그램은 무한 정밀도 숫자를 거의 다루지 않으며, 주로 업무 로직과 API를 만들고 급여를 계산함.
무언가를 셀 때 int16의 전체 범위조차 얼마나 자주 쓰는가? 영상 프레임도 size_t 값을 {1920x1080, 1920x1080x3 , 1920x1080x1.5, 1080}처럼 고정된 값으로 제한하기 쉬움. 420/RGB 프레임에서 흔히 쓰는 메모리 크기를 나타내는 값들임.
가능한 모든 상태의 무한한 공간을 검증하는 대신, 이 초입방체 안에 좁은 통로를 뚫듯 상태 공간을 제한하면 증명 범위를 크게 줄일 수 있음.