1. Getting to Know Lean🔗

관례에 따르면 프로그래밍 언어는 콘솔에 "Hello, world!"를 출력하는 프로그램을 컴파일하고 실행하며 소개한다. 이 간단한 프로그램으로 언어 도구가 올바르게 설치되었고 프로그래머가 컴파일된 코드를 실행할 수 있는지 확인한다.

그러나 1970년대 이후 프로그래밍은 변했다. 오늘날 컴파일러는 보통 텍스트 편집기에 통합되어 프로그래밍 환경이 프로그램을 작성하는 동안 피드백을 제공한다. Lean도 예외가 아니다. 확장된 언어 서버 프로토콜(Language Server Protocol)을 구현해 텍스트 편집기와 통신하고 사용자가 입력하는 동안 피드백을 제공한다.

Python, Haskell, JavaScript처럼 다양한 언어는 표현식이나 문장을 입력하는 읽기-평가-출력 반복(read-eval-print loop, REPL), 즉 대화형 최상위나 브라우저 콘솔을 제공한다. 언어는 사용자의 입력을 계산해 결과를 표시한다. 반면 Lean은 이 기능을 편집기와의 상호작용에 통합해 텍스트 편집기가 프로그램 본문에 통합된 피드백을 표시하도록 하는 명령을 제공한다. 이 장에서는 편집기에서 Lean과 상호작용하는 방법을 짧게 소개하고, 안녕, 세상!에서는 명령줄 배치 모드에서 전통적으로 Lean을 사용하는 방법을 설명한다.

편집기에서 Lean을 열어 각 예제를 따라 입력하며 이 책을 읽는 것이 좋다. 예제를 직접 실행해 보고 어떤 일이 일어나는지 확인하라!