2. 안녕하세요, 세계!🔗

Lean은 프로그래머가 즐겨 쓰는 텍스트 편집기를 벗어나지 않고도 언어로부터 상당히 많은 피드백을 받을 수 있는 풍부한 대화형 환경을 갖추도록 설계되었지만, 실제 프로그램을 작성할 수 있는 언어이기도 합니다. 즉, Lean에는 배치 모드 컴파일러, 빌드 시스템, 패키지 관리자를 비롯하여 프로그램 작성에 필요한 그 밖의 모든 도구도 갖추어져 있습니다.

이전 장에서는 Lean에서 함수형 프로그래밍의 기초를 다루었고, 이 장에서는 프로그래밍 프로젝트를 시작하고, 컴파일하고, 그 결과를 실행하는 방법을 설명합니다. 실행되면서 환경과 상호작용하는 프로그램(예: 표준 입력에서 입력을 읽거나 파일을 생성하는 프로그램)은 계산을 수학적 표현식의 평가로 이해하는 관점과 조화시키기 어렵습니다. 이 장에서는 Lean 빌드 도구에 대한 설명과 더불어, 세계와 상호작용하는 함수형 프로그램에 대해 생각하는 방법도 제시합니다.