1. Lean 알아가기🔗

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

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

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

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