Liquid Shplait으로 Shplait의 조건을 컴파일 때 검사한다

Liquid Shplait은 Shplait에 세분화 타입(refinement types)을 더합니다. Z3 솔버(solver)가 조건을 컴파일 시점(compile time)에 검사합니다. 예제에서는 입력과 반환값 모두 양의 정수라는 조건을 지정합니다. 저는 조건이 입력뿐 아니라 결과에도 붙는 점이 눈에 들어왔습니다. 함수가 내놓는 값까지 약속으로 적어 두기 때문입니다.

LLMLL은 AI 에이전트가 채운 코드가 계약을 어기면 병합 전에 거부하고, Liquid Shplait은 타입에 적은 조건을 컴파일 시점에 검사합니다. 하나는 병합 단계에서, 다른 하나는 언어의 컴파일 과정에서 작동합니다. 코드에 적은 규칙을 다음 단계로 넘기기 전에 확인한다는 점에서 두 소식이 맞닿습니다.

정수라는 종류에 더해 양수라는 조건도 타입에 적습니다. 예제에서는 입력과 반환값에 그 조건을 붙입니다. 조건을 적는 데서 끝나지 않고 컴파일 시점에 검사까지 이어진 점이 반갑습니다.

가장 먼저 갈리는 것은 설치 환경입니다. Racket 9.3 이상과 Z3가 모두 필요합니다. 검사기는 Z3 환경 변수, PATH 또는 일반적인 설치 경로에서 z3를 찾으므로, 경로를 직접 지정해야 하는 것은 아닙니다. 개인 시험은 간단해도 팀에 적용하려면 개발 환경과 빌드 환경에 이 의존성을 함께 두어야 합니다.

Racket 9.3 이상과 Z3를 준비한 뒤 liquid-shplait을 설치하고 예제 함수를 컴파일해 보십시오. 반환식을 0으로 바꾸어 다시 검사해 보십시오. 조건 위반 오류가 나오면 지정한 양수 조건이 검사된 것이고, 통과하면 문서에서 지원 범위를 확인하십시오.

타입 검사가 실행 전에 오류를 막아 준 경험은 마지막으로 언제였습니까?