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

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

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