coq와 같이 프로그램의 정확성을 입증하여 메모리 관리 문제를 해결 하시겠습니까?

Question

메모리 관리 문제 (메모리 누수, 매달려있는 포인터, double free() 등)를 해결할 수있는 타입 시스템으로 모든 프로그램의 정확성을 자동으로 증명할 수있는 언어를 구성 할 수 있는지 물어보고 싶었습니다. 통합 coq-like theorever prover과 같은 명제로서의 유형 (증명의 프로그램의 사고 방식에서)?

이 접근 방식에 근본적인 논리적 문제가 있습니까? (문제가 중단 되었습니까?) 아니면 실용 불가능합니까? 어떤 답변을 주셔서 감사합니다. 나는이 분야에 정통하지 않고, 단지 호기심을 알고 싶다. 유감스럽게 생각한다.)

Answer 1

예, 컴파일 할 언어에 대한 많은 연구가있었습니다. 시간 메모리 관리. 녹과 소유권 모델은이 분야에서 가장 중요한 산업 언어입니다. 항상 "linear types"을 조사하고 싶을 수도 있습니다.