50 증명하지 않은 것

50.1 신뢰 기반 — 증명이 기대는 것#

50.2 가장 큰 간극 — 모델과 구현 사이#

정리는 모델에 대한 것이다.
모델은 사람이 쓴 것이다.
컴파일러는 다른 언어로 쓴 다른 코드다.
그 둘이 같다는 것은 증명되지 않았다.

이음매를 잇는 장치들이다.

앞의 넷은 경험적이다. “지금 출력이 옳다” 가 아니라 “이 입력들에서 어긋나지 않았다” 를 말한다. 증명서 검산은 성격이 다르다. 그 자리를 때리는 입력이 없어도 말한다. 다만 그것도 사실을 믿고 추론만 검사한다. 두 층은 서로 다른 것을 잡는다. 증명이 못 잡은 결함을 대조가 잡았고, 대조가 못 잡은 결함을 증명이 잡았다. 겹쳐 쓰는 이유다.

가장 약한 이음매는 앞단(어휘·파서)이다. 두 백엔드 대조는 VM 과 네이티브를 비교하지만 둘은 같은 앞단을 지난다. 앞단이 틀리면 둘 다 똑같이 틀린다. 파서를 문법 모델과 직접 대조하려던 시도는 모델이 실제 문법보다 작아서 결론을 낼 만큼의 짝을 얻지 못했다. 이 자리를 닫으려면 앞단을 독립적으로 한 벌 더 구현해 대조해야 하고, 그 비용(두 벌을 유지하는 것)은 아직 치르지 않았다.

50.3 남은 것 — 주제별로#

module float_gap .
rem run: tenths
rem run: close_enough

fn tenths output bool .
do
  return eq (add 0.1 0.2) 0.3 .
end

fn close_enough output bool .
do
  let d f64 be sub (add 0.1 0.2) 0.3 .
  return lt (abs d) 0.000000001 .
end

$ lowentc --run tenths floats.low
tenths() = 0
$ lowentc --run close_enough floats.low
close_enough() = 1

0.1 과 0.2 를 더한 값은 0.3 과 같지 않다. 이것은 결함이 아니라 IEEE 754 의 성질이고, 그 성질은 이 언어의 증명이 다루지 않았다. 부동소수의 같음은 close_enough 처럼 허용 오차로 묻는다. 부동소수가 걸린 계산에서 이 책의 “증명됨” 은 아무것도 보증하지 않는다.

50.4 “전면 정적 안전” 으로 팔지 않는다#

정적으로 막는 것   차용 · 영역 · 참조 탈출 · 병렬 겹침 · 정수 넓히기
실행이 막는 것     증명 안 된 자리의 경계 검사 · 넘침 · 계약 검사
                   세대 핸들의 늘어진 참조

이 언어는 섞어 쓰는 설계다. 그리고 그것을 정적이라고 부르지 않는다. 비교를 정직하게 적으면, Rust 는 RustBelt 로 증명이 있고, Zig 는 안전을 주장하지 않는다(그것도 정직한 태도다). Lowent 는 “증명 있음 — 주로 순차 단편에 대해” 다. 그 조건절을 떼면 거짓말이 된다. 그리고 release_fast 빌드 모드는 남은 계약 검사를 없애 신뢰 경계를 하나 더 연다(14장). “미정의 동작이 없다” 는 말은 안전한 부분집합 안에서만 참이다.

50.5 그래서 무엇을 믿어도 되나#

✔ 정수가 조용히 값을 바꾸는 일은 없다               (수 · 증명됨)
✔ 번역을 통과한 코드에 차용 위반은 없다             (소유 · 증명됨, 순차)
✔ 효과 선언이 실제로 일어나는 효과를 덮는다         (효과 · 증명됨, 모델 안)
✔ 안전 코드에 데이터 경합은 없다                   (동시성 · 증명됨)
✔ 병렬 결과는 순차와 비트까지 같다                 (병렬 · 증명됨)
✔ 기본 차례면 순서대로 사고해도 된다               (약한 메모리 · 증명됨, ∀실행)
✔ 경계 검사를 지운 자리는 범위 안임이 논증된 자리   (경계 · 증명됨 + 검산)

△ 컴파일러가 이 모델을 정확히 따라간다             (경험적)
△ 약한 차례를 명시한 코드                          (SPSC 하나만 증명 — 나머지는 감사 대상)
✘ 부동소수의 세부                                   (다루지 않았다)

마지막 줄들이 있는 문서를 믿어도 된다. 없는 문서는 다시 봐야 한다.