8. Programming, Proving, and Performance🔗

이 장은 프로그래밍을 다룬다. 프로그램은 올바른 결과를 계산해야 할 뿐 아니라 효율적으로 계산해야 한다. 효율적인 함수형 프로그램을 작성하려면 자료구조를 적절히 사용하는 법과 프로그램 실행에 필요한 시간과 공간을 생각하는 법을 모두 알아야 한다.

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

프로그램을 빠르게 만들도록 다시 작성하면 코드를 이해하기 어려워지는 경우가 많다. 증명은 서로 다른 알고리즘이나 구현 기법을 사용하더라도 두 프로그램이 항상 같은 답을 계산함을 보일 수 있다. 이렇게 느리지만 단순한 프로그램을 빠르고 복잡한 버전의 명세로 사용할 수 있다.

증명과 프로그래밍을 결합하면 프로그램을 안전하면서도 효율적으로 만들 수 있다. 증명을 이용하면 실행 시점 범위 검사를 생략할 수 있고 많은 테스트가 필요 없게 되며, 실행 성능 오버헤드 없이 프로그램에 매우 높은 신뢰도를 부여할 수 있다. 그러나 프로그램에 관한 정리를 증명하는 일은 시간과 비용이 많이 들 수 있으므로 다른 도구가 더 경제적인 경우도 많다.

대화형 정리 증명은 깊은 주제다. 이 장에서는 Lean으로 프로그래밍할 때 실제로 마주치는 증명에 초점을 맞춰 맛보기만 제공한다. 흥미로운 정리 대부분은 프로그래밍과 밀접하게 관련되지 않는다. 더 배울 자료 목록은 다음 단계를 참고하라. 프로그래밍을 배울 때와 마찬가지로 증명 작성은 직접 해 보는 경험을 대신할 수 없으니, 이제 시작하자!