완성 가능한 프로그래밍 언어

A Perfectable Programming Language

📅 2026-04-12 📰 Hacker News (Top) ⬆ 11

요약

Lean 프로그래밍 언어가 의존 타입, 정리 증명, 메타프로그래밍을 통해 '완성 가능한' 언어라고 주장합니다. 이를 통해 코드 자체에 대한 속성을 언어 내에서 표현하고 증명할 수 있습니다.

핵심 포인트

Lean의 의존 타입으로 함수의 동작을 정리로 표현하고 증명 가능 (예: returnFive 함수가 항상 5를 반환함)
메타프로그래밍을 통한 seamless한 커스텀 신택스 지원 (예: 틱택토 보드를 자연스러운 표기법으로 작성)
점진적 최적화 가능성이 있어 성능 개선의 여지가 크다는 강점

왜 중요한가

코드의 정확성을 형식으로 증명할 수 있는 의존 타입 언어의 실제 활용 사례를 보여주며, 안전성이 중요한 시스템 개발에 참고가 됩니다.

📄 전문 번역

완벽해질 수 있는 프로그래밍 언어

Alok Singh

2026-04-02

파티에서 Sydney Von Arx가 물었어요. 프로그래밍 언어 40개를 댈 수 있냐고요. 뭐, 실리콘밸리니까요.

Racket, Agda, Clean, Elm, TypeScript, sh, ASP, Verilog, JavaScript, Scheme, Rust, Nim, Intercal, sed, Isabelle, Visual Basic, zsh, Alokscript, Coq, Idris, Hack, Prolog, Whitespace, PureScript, Go, Odin, Haskell, Python, tcsh, Unison, Clingo, bash, Java, Zig, Cyclone, PHP, awk, C, ActionScript, C++.

하지만 정말 최고는 Lean이에요.

왜 Lean일까요?

완벽해질 수 있기 때문입니다. 지금 완벽한 건 아니지만, 더 나아질 여지가 충분하다는 뜻이죠.

Lean의 가장 큰 특징은 Lean으로 작성한 코드의 특성들을 Lean 자체 안에서 기술할 수 있다는 거예요. 코드에 대한 사실과 성질들이 차곡차곡 쌓이는데, 이런 누적을 우리는 "진보"라고 부릅니다.

코드 자신에 대해 말하기

모든 언어에서 결국 이런 상황이 옵니다. "이 함수는 항상 5를 반환해"라고 말하고 싶은데, 대부분의 언어에선 그 사실을 프로그래밍에 실제로 활용할 방법이 없어요.

예를 들어 TypeScript에선 이렇게 쓰죠:

function returnFive(x : number) : number {
  return 5;
}

그런데 Lean에선?

def returnFive (x : Int) : Int := 5

theorem returnFive_eq_five (x : Int) : returnFive x = 5 := rfl

example (a : Int) : 6 = returnFive a + 1 := by
  unfold returnFive
  rfl

정말 다르죠? Lean에선 함수가 항상 5를 반환한다는 걸 정리(theorem)로 증명할 수 있고, 그걸 바탕으로 다른 수식을 증명할 때 실제로 활용할 수 있습니다.

타입 시스템의 진화 방향

흥미롭게도 타입이 없던 언어들도 자연스럽게 타입을 들이게 돼요. PHP 7.4도 타입을 추가했고, Python도 타입 주석을 지원합니다. 전반적으로 TypeScript와 Rust 같은 타입 강력한 언어로의 흐름이 맞습니다.

사람들은 계속 타입 시스템을 더 강력하게 만들고 싶어 해요. Go도 그렇고, C++ 템플릿은 그 극단적인 사례입니다. 컴파일 타임에 계산할 수 있으면, 누군가는 반드시 그렇게 하고 싶어 하죠. Rust의 지속적인 const 화도 같은 맥락입니다.

뭔가를 제대로 하려면? 가장 쉬운 방법은 처음부터 제대로 하는 거예요. "제대로"라는 게 사실 의존 타입(dependent types)을 의미합니다. 더 정교한 개념도 있지만, 튜링 완전성처럼 의존 타입만 있어도 거의 모든 걸 표현할 수 있거든요. 그래서 Lean은 계속 완벽해질 수 있는 거입니다.

정리(Theorem) 시스템

타입 위에 필요한 건 "이 두 타입이 같은가"를 보여줄 수 있는 인프라예요. 이건 기본적으로 정리 증명기(theorem prover)를 의미합니다. 의존 타입을 가진 모든 언어가 정리 증명기가 될 수 있지만, 그러려면 우리가 "정리 증명 인프라"라고 부르는 좋은 API를 갖춰야 합니다.

이제 문법 얘기

정리 시스템은 "의미론" 쪽이라면, 문법 쪽에는 메타프로그래밍(metaprogramming)과 커스텀 문법(custom syntax)이 있습니다.

메타프로그래밍

대부분의 언어는 메타프로그래밍을 제대로 지원하지 못합니다. Rust의 절차형 매크로도 좀 어색한 편이죠.

그런데 Lean은? 정말 부드럽고 자연스럽습니다. 틱택토 게임을 커스텀 보드 문법으로 만드는 예제를 보세요:

inductive Player where
  | X
  | O
  deriving BEq, Inhabited

inductive Square where
  | empty
  | occupied (player : Player)
  deriving BEq, Inhabited

@[simp] def boardSize : Nat := 9

structure Board where
  squares : Array Square
  deriving BEq

이제 커스텀 문법을 정의합니다:

declare_syntax_cat tttCell
syntax "X" : tttCell
syntax "O" : tttCell
syntax "_" : tttCell

declare_syntax_cat tttRow
syntax (name := tttRowRule) tttCell "|" tttCell "|" tttCell : tttRow

declare_syntax_cat tttBoardSyntax
syntax tttRow tttRow tttRow : tttBoardSyntax

private def elabTttCell (stx : Lean.Syntax) : Lean.Elab.Term.TermElabM Square :=
  match stx with
  | `(tttCell| X) => pure (.occupied .X)
  | `(tttCell| O) => pure (.occupied .O)
  | `(tttCell| _) => pure .empty
  | _ => Lean.throwError s!"unsupported cell syntax {stx}"

open Lean Elab Term in
elab "board! " b:tttBoardSyntax : term => do
  let mut squares : Array Square := #[]
  unless b.raw.getNumArgs = 3 do
    Lean.throwError s!"Expected 3 rows, got {b.raw.getNumArgs}"
  for rowIdx in [:3] do
    let row := b.raw.getArg rowIdx
    unless row.isOfKind `tttRowRule do
      Lean.throwError s!"malformed tttRow"
    let cells := #[row.getArg 0, row.getArg 2, row.getArg 4]
    for cell in cells do
      squares := squares.push (← elabTttCell cell)
  unless squares.size = boardSize do
    Lean.throwError s!"internal error: expected 9 squares, got {squares.size}"
  let squareTerms ← squares.mapM fun sq =>
    match sq with
    | .empty => `(Square.empty)
    | .occupied .X => `(Square.occupied Player.X)
    | .occupied .O => `(Square.occupied Player.O)
  let arrSyntax ← `(#[$squareTerms,*])
  let boardTerm ← `(Board.mk $arrSyntax)
  Lean.Elab.Term.elabTerm boardTerm none

이제 이렇게 사용할 수 있어요:

#eval getGameStatus (board!
  X | O | _
  _ | X | _
  O | _ | X)
-- Win X

이런 식으로 API를 여러 계층으로 설계하고 문법 뒤에 숨길 수 있습니다. 필요하면 문법의 해석도 쉽게 바꿀 수 있죠. Lean의 타입 시스템이 메타프로그래밍도 잘 지원하긴 하지만, 솔직히 Lean 문법을 위한 메타-메타프로그래밍이 더 있으면 정말 좋겠어요.

def «🎮 tic tac toe 🎮» : Board := board!
  X | O | X
  O | X | O
  X | _ | O

#eval getGameStatus «🎮 tic tac toe 🎮»
-- Win X

왜 정리 증명기일까?

사실 제대로 하려면 자연스럽게 정리 증명기가 되는 거예요. 프로그래밍 언어 진화를 보면 여러 갈래에서 정리 증명 기능으로 수렴하는 모습이 보입니다.

성능

이게 가장 중요한 부분입니다. 느린 언어는 정말 별로거든요. 컴퓨터를 쓰는 이유가 뭐겠어요.

Lean은 더 빨라질 여지가 있습니다. Rust만큼 빠르진 않지만, 두 코드가 같다는 걸 증명할 수 있다는 특징 덕분에 최적화 가능성이 정말 높아요.

theorem five_plus_one_eq_six : ∀ a : Int, returnFive a + 1 = 6 := by
  intro a
  unfold returnFive
  rfl

이런 증명을 통해 컴파일러가 더 공격적인 최적화를 할 수 있게 돕는 거죠. Lean의 미래는 정말 밝습니다.

🔗 원문 보기 👍 유용해요