정지 문제와 괴델 정리로 설명하는, 올바른 소프트웨어를 쓰기가 어려운 이유

형식 검증에 계속 관심은 있는데 직접 해본 건 장난감 수준 증명뿐임. 검증 가능한 프로그램을 애초에 설계하는 게 진짜 어려운 설계 문제고, 'AI가 알아서 해줄 테니 머리 끄고 있어도 된다'는 가정은 좀 위험하다고 봄.

정지 문제라는 용어가 좀 낡은 것 같음. 요즘 프로그램은 안 끝나는 게 정상이라 halting이라고 하면 그냥 멈췄거나 데드락 걸린 상태로 읽히더라.

CS 용어가 소프트웨어 개발 쪽으로 잘 안 옮겨지는 게 많음. CS를 개발 입문 경로처럼 취급한 게 양쪽 분야에 다 손해였음.

정지 문제는 엄밀한 CS 용어고 낡지 않았음. 원자로가 '임계'에 도달했다는 말을 비전공자가 오해한다고 용어가 잘못된 건 아니잖아. 함수는 여전히 입력 받고 출력 내는 대상이고 거기에 정지 문제가 적용됨.

무작위로 답을 고르면 정답 확률이 몇이냐는 25/50/0/25 밈도 결국 괴델 불완전성 정리의 다른 버전 같음. 규칙 체계가 자기 자신을 추론하지 못하는 문제임.

안 끝나는 소프트웨어는 공동귀납 타입으로 모델링하면 됨. Stream이 대표적인 예임.

성공적으로 멈추느냐랑 그냥 멈추느냐는 다른 문제임. 어느 쪽이든 판정 불가능하고, 성공 여부까지 물으면 더 어려운 문제가 됨.

수학적 정확성과 현실에서 돌아가는 것 사이에는 단단한 구분이 있다고 봄. 형식적 정확성이 언제 유용하고 언제 골칫거리인지 판단하는 게 핵심임.

금융에서 학계 출신 개발자들이랑 일한 경험인데, 형식 증명 강조가 심해서 복잡도만 올리고 진도는 안 나갔음. 게다가 증명이 현실에서 안 맞는 가정 위에 세워져 있었음.

네트워크에 노출되거나 외부 데이터를 처리하는 소프트웨어는 최소한 공격자가 원하는 코드를 실행하지 못하게는 해야 함. 완전한 정확성 증명이 아니어도 많은 성질을 증명해야 됨.

군사, 의료, 산업 자동화는 예전부터 수학적 정확성이 필요했음. 이 글은 LLM 시대에 오히려 더 잘 맞는 얘기임. 토큰 기반 상징 추론의 근본 한계를 보여줌.

요즘 소프트웨어는 형식 모델에서 멀어지는 쪽으로 발전했음. 파일시스템은 모든 프로세스가 공유하는 객체라 명세 만들기가 사실상 불가능하고, root 권한도 언제든 얻을 수 있어서 상태를 다 제거하는 증명이 어려움.

API는 완벽하게 만들고 현실 세계 적응은 그 API를 감싸는 모듈 안에서 처리하는 식으로 둘을 섞을 수 있음.

정확성이 충분조건은 아니지만 필요조건임. 프로그램이 애초에 올바르지 않으면 의도대로 동작할 가능성은 거의 없음.