8. 프로그래밍, 증명, 그리고 성능🔗

이 장에서는 프로그래밍을 다룹니다. 프로그램은 올바른 결과를 계산해야 하지만, 그 계산을 효율적으로 수행하는 것도 중요합니다. 효율적인 함수형 프로그램을 작성하려면 자료 구조를 적절히 사용하는 방법과 프로그램 실행에 필요한 시간과 공간을 따져 보는 방법을 모두 알아야 합니다.

이 장은 증명에 관한 내용이기도 합니다. Lean에서 효율적인 프로그래밍을 위한 가장 중요한 자료 구조 중 하나는 배열이지만, 배열을 안전하게 사용하려면 배열 인덱스가 범위 안에 있음을 증명해야 합니다. 게다가 배열을 다루는 흥미로운 알고리즘은 대부분 구조적 재귀 패턴을 따르지 않고, 대신 배열을 반복 순회합니다. 이러한 알고리즘은 종료되지만, Lean이 이를 항상 자동으로 확인할 수 있는 것은 아닙니다. 증명을 사용하면 프로그램이 종료되는 이유를 보일 수 있습니다.

프로그램을 더 빠르게 만들기 위해 다시 작성하면 이해하기 더 어려운 코드가 되는 경우가 많습니다. 증명은 두 프로그램이 서로 다른 알고리즘이나 구현 기법을 사용하더라도 항상 같은 답을 계산한다는 것을 보여 줄 수도 있습니다. 이런 방식으로 느리지만 단순한 프로그램이 빠르지만 복잡한 버전의 명세 역할을 할 수 있습니다.

증명과 프로그래밍을 결합하면 프로그램을 안전하면서도 효율적으로 만들 수 있습니다. 증명이 있으면 런타임 경계 검사를 생략할 수 있고, 많은 테스트가 필요 없어집니다. 또한 런타임 성능 오버헤드 없이 프로그램을 매우 높은 수준으로 신뢰할 수 있습니다. 하지만 프로그램에 대한 정리를 증명하는 일에는 시간과 비용이 많이 들 수 있으므로, 다른 도구를 쓰는 편이 더 경제적인 경우가 많습니다.

대화형 정리 증명은 깊이 있는 주제입니다. 이 장에서는 Lean으로 프로그래밍하면서 실제로 마주치는 증명을 중심으로 맛보기만 제공합니다. 흥미로운 정리 대부분은 프로그래밍과 밀접한 관련이 없습니다. 더 배울 수 있는 자료 목록은 다음 단계를 참고하십시오. 하지만 프로그래밍을 배울 때와 마찬가지로, 증명 작성법을 배울 때도 직접 해 보는 경험을 대신할 수 있는 것은 없습니다. 이제 시작해 봅시다!