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

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

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

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

증명과 프로그래밍을 결합하면 프로그램을 안전하면서도 효율적으로 만들 수 있습니다. 증명을 이용하면 런타임 범위 검사를 생략할 수 있으며, 많은 테스트를 불필요하게 만들고, 런타임 성능 오버헤드를 전혀 발생시키지 않으면서도 프로그램에 대한 극히 높은 수준의 확신을 제공합니다. 하지만 프로그램에 대한 정리를 증명하는 일은 시간이 많이 걸리고 비용이 많이 들 수 있으므로, 다른 도구가 더 경제적인 경우가 많습니다.

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