2. Hello, World!🔗

Lean은 프로그래머가 좋아하는 텍스트 편집기를 벗어나지 않고도 언어에서 많은 피드백을 받을 수 있는 풍부한 대화형 환경으로 설계되었지만 실제 프로그램도 작성할 수 있는 언어다. 따라서 배치 모드 컴파일러, 빌드 시스템, 패키지 관리자와 프로그램 작성에 필요한 다른 모든 도구도 갖추고 있다.

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