의존성의 정리를 인용하기 전에 공리부터 본다

컴파일되는 정리가 곧 증명된 정리라는 보장은 없다. sorry는 어떤 목표든 닫고, Lean은 경고 하나와 함께 파일을 받아들인다. 다른 곳에서 빌드된 의존성이라면 그 경고는 눈앞에 없다.

확인 수단은 #print axioms다. 정리가 쓰는 모든 상수를 전이적으로 따라가서 거기 닿는 공리를 나열한다.

theorem small : 2 + 2 = 4 := rfl
theorem big : 2 ^ 64 % 7 = 2 := by native_decide

#print axioms small
#print axioms big

첫 번째는 공리가 없다고 나온다. 두 번째는 Lean.ofReduceBool을 나열한다. native_decide는 결정 절차를 컴파일된 코드로 실행하고, 커널은 그 결과를 믿고 받는다. 밑 어딘가에 sorry가 있으면 sorryAx로 드러난다.

흔히 보는 셋은 propext, Classical.choice, Quot.sound다. 목록에 그 밖의 것이 있으면 결과의 일부가 커널의 검사 없이 받아들여졌다는 뜻이다.

이어지는 대화 1

서로의 근거를 따라

Alden고유 링크
의존성의 unsafe에 대해 Rust가 주지 않는 검사가 이것입니다. #print axioms는 정리 하나 단위로 그것을 모아 줍니다. 인용하는 정리마다 손으로 돌리는 것입니까, 아니면 목록이 늘어날 때 빌드가 실패하게 할 수 있습니까?

보안과 검증
타입을 붙인 병합 함수가 `__proto__`까지 따라가는 문제
설정 가져오기 기능이 작은 재귀 병합 함수를 써요. 매개변수 타입은 꼼꼼해 보이지만 프로그램이 기대하는 걸 적어 둔 것일 뿐이에요. 루프는 파싱된 파일에 실제로 있는 키를 그대로 돌아요. JSON.parse는 __proto_…
Tess답글 2typescript javascript
보안과 검증
sleep 없이 Go 채널 인계 테스트하기
제가 보는 핸드오프 테스트는 대부분 sleep 하나와 희망 섞인 단언으로 끝나요. 이건 그게 없어도 돼요. 요청에는 식별자가 붙어 있어요. 워커는 버퍼 없는 채널에서 요청을 받아 그 식별자를 요청의 결과 슬롯에 쓰고, 같은…
Vadim답글 23go
보안과 검증
컴파일러는 왜 부호 있는 오버플로 검사를 지웠을까?
부호 있는 int에 대한 if (x + 1 < x)는 오버플로 방어가 아니다. C에서 부호 있는 정수 오버플로는 정의되지 않은 동작이므로, 컴파일러는 x + 1이 절대 넘치지 않는다고 가정하고 조건을 거짓으로 결론 내린 뒤…
Lio답글 4c