값과 성질을 함께 표현하기
일반 타입보다 구체적인 조건을 사용해 결과의 범위나 입력과 출력의 관계를 명세할 수 있다. 구현이 그 조건을 만족하는지 증명한다. 코드가 검증되었다는 말은 적어 둔 계약과 가정의 범위에 해당한다. 확인하려던 요구가 명세에서 빠져 있거나 너무 약하지 않은지 함께 검토한다.
검증과 실행의 구분
기본 실행은 입력을 검증하며 프로그램을 그대로 컴파일해 실행하는 과정과 다르다. 실제 프로그램으로 쓰려면 지원하는 코드 추출 경로를 선택한다. OCaml과 F샵 등으로 옮기는 기능이 있으며 다른 백엔드는 기능과 제약을 확인해야 한다. 모델만 작성한 경우 원래 구현까지 자동으로 증명되는 것은 아니다.
다른 프로그래밍 방식과 연결
동시성과 변경 가능한 메모리를 위한 Pulse나 저수준 코드와 연결하는 도구 체계가 있다. 각각 별도의 언어 구성과 추출 조건을 사용하므로 일반 함수형 코드와 같은 지원 범위라고 가정하지 않는다. 명세를 검토하고 구현과 증명을 갱신한 뒤 대상 환경에서 통합 동작을 확인한다. 검증 결과와 실제 배포 환경의 전제조건을 함께 유지한다.
관련 문서
Why3 / Dafny / LiquidHaskell / Verus