왜 모든 것이 커널 안에 있는가?

Why is it all in the kernel?

Collatz 추측이 반증되었다는 sensational한 소식이 전해졌지만, 증명은 Lean 커널의 버그로 인해 틀렸다. 이 사건은 증명 객체가 독립 검증을 통해 건전성을 보장한다는 믿음이 허구임을 드러낸다. 저자는 증명 객체가 메모리 부담을 주고 오히려 버그를 유발할 수 있다고 주장하며, 집합론이나 단순 타입 이론처럼 최소한의 공리에서 출발해 귀납 정의와 재귀 함수를 '정직한 노동'으로 구성하는 방식을 옹호한다. Isabelle/HOL은 이러한 방식으로 커널 외부에서 재귀 함수를 지원하며, 건전성에 더 중점을 둔다면 HOL Light나 HOL4를 선택하라고 조언한다.