2019 년 1 월 현재 Michelson with Coq의 공식 검증 구현은 아직 완료되지 않았습니다. 그러나 Coq 대화식 정리 증명을 사용하여 다음 언어 부분이 형식화됩니다.
타입 시스템
문법
의미론
Coq는 Gallina라고하는 프로그램 사양과 더 높은 수준의 수학적 언어를 구현합니다.이 언어는 차례로 고급 구조 논리와 풍부한 유형의 기능적 프로그래밍 언어를 결합한 계산적 구조 계산법 (Colculus of Inductive Constructions)이라는 표현 형식 언어를 기반으로합니다. Coq는 고유 한 명령 언어를 통해 다음을 수행 할 수 있습니다.
효율적으로 평가 될 수있는 함수 또는 술어를 정의합니다.
상태 수학 이론 및 소프트웨어 사양;
대화식으로 이러한 정리의 공식적인 증거를 개발합니다.
상대적으로 작은 인증 "커널"로 이러한 증명을 기계 검사합니다.
인증 된 프로그램을 Objective Caml, Haskell 또는 Scheme과 같은 언어로 추출합니다.
증명 개발 시스템으로서 Coq는 대화식 증명 방법, 의사 결정 및 반 결정 알고리즘 및 사용자가 고유 한 증명 방법을 정의 할 수있는 전술 언어를 제공합니다. 외부 컴퓨터 대수 시스템 및 정리 프로 버와의 연결도 가능합니다.
Coq는 수학 공식화 및 프로그램 개발을위한 플랫폼으로서 고급 표기법, 암시 적 내용 및 기타 유용한 매크로를 지원합니다. 이 저장소는 Coq 대화식 정리 검증 자 (https://framagit.org/rafoo/michelson-coq)를 사용하여 Michelson을 공식화 한 것입니다.
