1. Lean 알아가기🔗

전통에 따르면, 프로그래밍 언어는 콘솔에 "Hello, world!"를 표시하는 프로그램을 컴파일하고 실행하는 것으로 소개되어야 합니다. 이 간단한 프로그램은 언어 도구가 올바르게 설치되었는지, 그리고 프로그래머가 컴파일된 코드를 실행할 수 있는지를 확인합니다.

그러나 1970년대 이후 프로그래밍은 변화해 왔습니다. 오늘날 컴파일러는 일반적으로 텍스트 편집기에 통합되어 있으며, 프로그래밍 환경은 프로그램을 작성하는 동안 피드백을 제공합니다. Lean도 예외는 아닙니다. Lean은 언어 서버 프로토콜(Language Server Protocol)의 확장 버전을 구현하여 텍스트 편집기와 통신하고 사용자가 입력하는 동안 피드백을 제공할 수 있도록 합니다.

Python, Haskell, JavaScript처럼 다양한 언어는 대화형 최상위 수준(interactive toplevel) 또는 브라우저 콘솔이라고도 불리는 read-eval-print-loop(REPL)을 제공하며, 이를 통해 식이나 문장을 입력할 수 있습니다. 그런 다음 언어는 사용자 입력의 결과를 계산하여 표시합니다. 반면 Lean은 이러한 기능들을 편집기와의 상호작용에 통합하여, 텍스트 편집기가 프로그램 텍스트 자체에 통합된 피드백을 표시하도록 하는 명령을 제공합니다. 이 장에서는 편집기에서 Lean과 상호작용하는 방법을 간략히 소개하며, Hello, World!에서는 전통적인 방식으로 명령줄에서 배치 모드로 Lean을 사용하는 방법을 설명합니다.

편집기에서 Lean을 열어 놓고 이 책을 읽으면서 각 예제를 직접 따라 입력해 보는 것이 가장 좋습니다. 예제들을 이리저리 다루어 보고 어떤 일이 벌어지는지 확인해 보십시오!