태그: #liquid-haskell
GPU·LLM·MLOps·쿠버네티스, 그리고 마음가짐에 관한 글 · 2 편
Lean 4 & 정리 증명기 2026 — mathlib / Rocq (구 Coq) / Agda / Isabelle / FStar / AlphaProof / AIMO 심층 가이드
2026년, 정리 증명기(proof assistant)는 더 이상 학계의 비밀 무기가 아니다. Lean 4는 Leonardo de Moura가 AWS로 옮긴 뒤 폭발적으로 성장했고, mathlib는 100만 개 정리를 넘기며 Terence Tao를 비롯한 일급 수학자들의 일상 도구가 되었다. Coq는 2024년 3월 Rocq로 리브랜드를 마쳤고, Agda·Idris 2·Isabelle/HOL
2026-05-16 · 37 분 읽기 #lean-4#lean#mathlib#rocq#coq모던 Haskell 2026 — GHC 9.10 / 9.12 / GHCup / Cabal 3.14 / Stack / IHP / Servant / Effectful / Pandoc / Cardano 심층 가이드
2026년의 Haskell은 더 이상 "박사학위 받은 사람들이 논문 쓰려고 쓰는 언어"가 아니다. GHC 9.10(2024년 5월)과 9.12(2024년 12월)로 컴파일러는 한 단계 더 빨라졌고, GHCup이 공식 권장 설치 도구로 자리 잡으면서 Stack과 Cabal 3.14 사이의 선택이 단순해졌다. IHP가 Rails 같은 풀스택 경험을 제공하고, Servant가 타입드 HTTP AP
2026-05-16 · 32 분 읽기 #haskell#ghc-9-10#ghc-9-12#ghcup#cabal