Lean 4.22: 명령형 프로그램을 위한 새로운 검증 인프라

Lean 4.22는 명령형 프로그램의 속성을 증명하기 위한 흥미로운 새로운 기능인 새로운 검증 인프라를 도입합니다. 이 글에서는 리스트에 합이 0이 되는 두 정수가 있는지 확인하는 간단한 예를 사용하여 이 기능의 사용 방법을 보여주고 Dafny 및 Verus와 같은 유사한 도구와 비교합니다. 새로운 프레임워크인 Std.Do는 Hoare triple을 활용하고 `mvcgen` 및 `grind` 전술을 결합하여 루프 및 조기 반환과 같은 복잡한 제어 흐름을 가진 명령형 프로그램의 검증 프로세스를 크게 간소화합니다. 외부 SMT 솔버에 의존하는 자동화된 시스템과 달리 Lean의 대화형 증명 접근 방식은 더 높은 신뢰성, 더 쉬운 디버깅 및 더 나은 유지 관리를 제공하여 실제 프로그램 검증 작업에 매력적인 선택이 됩니다.