형식 기법과 프로그래밍의 미래

수십 년 전에 정확성 증명 작업을 했고, 당시 시스템이 이후의 많은 시스템보다 증명 자동화가 더 많았음
쉬운 부분은 최초의 SAT 솔버인 Oppen-Nelson 단순화기가 해결했고, 어려운 부분은 휴리스틱과 이전 보조정리를 쓰는 Boyer-Moore 증명기가 맡았음. 사람의 어려운 일은 증명기가 시도해보고 이후 증명에 쓸 보조정리를 제안하는 것이었음
이후 시스템들은 자동화가 줄어든 듯했고, 형식 기법이 빗나간 이유는 실무보다 형식주의에 너무 빠졌기 때문이라고 봄. 상업 프로젝트에서 버그 없는 코드를 원했던 입장에서는, 학계식 프로젝트가 논문용 간결한 표기와 적은 경우 분석을 선호하는 수학자 편향에 빠졌다고 느꼈음
실제로는 많은 자동화된 갈아넣기가 필요하고 통찰은 적게 필요해야 함. 영리한 사람들이 종이와 연필 증명의 장황함을 피하려고 양상 논리, 시간 논리 같은 새 논리를 계속 만들었지만 별로 도움이 되지 않았음. 이 분야의 기본 진실은 대부분의 정리가 꽤 평범하다는 것임
Jane Street 사람들이 말하듯 언어를 통제할 수 있다는 점이 큰 장점임. 검증 문장은 프로그래밍 언어 안에 통합되어야 하고, 주석이나 다른 문법, 별도 파일에 박혀 있으면 불필요한 일이 늘어남. Jane Street가 이 방향을 밀어붙이는 건 좋아 보임
40년도 더 전에 너무 일찍 이 일을 했고, 당시에는 Boyer-Moore 증명기로 숫자 이론을 처음부터 쌓는 데 계산 시간이 45분쯤 걸렸지만 이제는 1초도 안 걸림 https://archive.org/details/manualzilla-id-5928072/page/n3/m...

형식 기법을 오래 해온 입장에서, 새 논리가 도움이 안 된다는 말에는 조금 동의하기 어려움. 산업용 논리는 실용적이고, 시스템이 만족해야 할 정교한 속성을 매우 간결하게 쓸 수 있게 해줌
논리는 컴퓨터 과학과 소프트웨어 공학에서 물리학·기계공학·토목공학의 미적분 같은 위치에 있음. LTL이나 최근의 분리 논리 같은 것들은 엄청난 돌파구였음
인기를 꽤 얻은 TLA+ 가 그 증거이고, 모델 검사는 매우 실용적임. 지금 흥미로운 점은 더 무거운 형식 기법, 특히 정리 증명이 일반 시스템 소프트웨어에서도 쓸 만큼 저렴해질 수 있다는 것임
함수에 대한 형식 명세를 쓰고 SAT/SMT, 정리 증명기, LLM의 하이브리드로 합성하고 정확성을 증명받는 방식이 머지않아 표준이 될 수도 있음
On the Unusual Effectiveness of Logic in Computer Science: https://www.cs.rice.edu/~vardi/papers/aaas99.jsl.pdf
From Philosophical to Industrial Logics: https://www.cs.rice.edu/~vardi/papers/icla09.pdf

형식 명세에서는 사람이 해석하고 작성할 수 있음이 정말 중요해질 것임
걱정되는 건 해독하기 어려운 수학이 생기고, 소수의 신봉자 집단이 그것을 지키는 상황임. 서로 다른 난해한 표기들은 호환되지 않고, 하나를 이해해도 다른 것을 이해하는 데 별 도움이 안 될 수 있음. 대부분은 제대로 검증할 수 없는 영어 문장만 쓰게 될 것임
더 나쁘게는 기계에게 자기 문장을 형식화하게 해놓고, 그 형식주의나 증명은 이해하지 못한 채 검증 연극에 참여하다가 모든 것이 터지면 놀라는 척할 수도 있음

Ada/SPARK를 봤는지 궁금함. 봤다면 일이 어떻게 되어야 하는지에 대한 직관과 맞는지도 궁금함
타입 시스템이 빠르게 다루지 못하는 부분에 이런 능력을 통합하려는 작업을 천천히 하고 있어서, 이 길을 먼저 가본 사람들의 관점이 관심 있음

좋음. 최근 몇 달 동안 Scala 3에서 표현력 높은 타입을 써서 타입이 점점 더 많은 컴파일 시간 증명을 담도록 옮겨왔음. 매크로는 쓰지 않지만 몇 개는 쓸 만함
이 방식은 에이전트형 테스트가 퍼져나가는 문제를 줄이는 데만 도움이 되는 게 아니라, 에이전트가 낮은 품질의 작업 방식으로 떨어지는 것도 막는 듯함. 특히 에이전트가 합리적으로 일반화해야 할 때도 모든 것에 새 단형 타입을 만들려는 명사 축적을 막고 있음
좋은 품질의 에이전트 코딩을 가속하는 쪽은 형식 기법을 닮은 도구들, 강한 타입 시스템을 가진 언어까지 포함한 쪽이라고 봄
여기서 표현력 높은 타입이란, 팀이 이미 타입 수준 프로그래밍에 익숙하지 않다면 일반 코드베이스에 넣고 싶지는 않은 기법들을 뜻함. 즉 고차 종류 타입과 타입 함수가 이상한 물건이 아니라 기본 블록인 팀이어야 함
에이전트는 지식 면에서 대부분의 개발자보다 “수학”을 잘하고, 범주론에 물든 개발자보다도 나은 경우가 많음. 더구나 대화에 대해 “무한한” 인내심이 있다고 보면 교육도 꽤 잘함
개인적으로는 Codex에게 취미 증명 몇 개를 Lean식으로 바꾸게 했는데 매우 쉬웠음. 100% “정확하다”고 말하는 건 아니고, 더 철저히 확인하려면 Lean 4를 더 배워야 하지만, 기본적으로 고전적인 증명 함정도 점검하는 듯함. 형식 기법의 미래가 매우 기대됨

Gen AI가 코드를 많이 만들기 때문에 인간의 가치를 검증 쪽으로 옮기자는 이야기로 보임. 프로그래밍이 정말 무엇인지 가끔 생각함
영어가 모국어가 아닌 입장에서는 프로그래밍을 배우는 것 자체가 큰 도전임. 번역되지 않은 영어 문서를 이해하려면 기계번역에 의존해야 하고, 내 언어로 된 자료는 5~6년쯤 뒤처져 있음
이제 AI가 만든 수만 줄의 코드를 코드 리뷰하는 게 불가능하니, 수학적 증명 같은 절대 규칙을 세우자는 논의가 보임. 이 글을 읽으니 Rust의 borrow checker가 떠오름. 실제로 Rust를 몇 번 써보면 사람들이 borrow checker를 피하려고 꼼수를 쓰는 나쁜 습관으로 이어지곤 함
수학적 엄밀성이 지나치면 사람은 우회로를 찾게 됨. 나처럼 교육이 부족한 프로그래머는 특히 그러기 쉬움
이런 시도는 결국 특정한 형식화된 답만을 위한 코드를 쓰는 결과가 될 것 같음. 그렇게 표준화되면 인간의 요구에 대응할 수 있을지 확신이 안 섬
이런 방어적 프로그래밍 시도는 괜찮지만, 내가 만든 표현으로는 공격적 프로그래밍을 하고 싶음. 위험을 감수하되 빨리 고치고 배포하며, 시간이 지나면 충분히 좋아질 것이라고 믿는 방식임
물론 Jane Street처럼 정확도가 중요하고 업무 범위가 잘 정의된 기존 산업에서는 이 글의 접근이 맞음. 시장의 요구를 적절히 모델링할 만큼 데이터가 충분하기 때문임
하지만 돈을 벌려고 금광을 찾아 계속 이동하는 나 같은 사회적 패배자에게는 이런 방법론이 사치처럼 보임. 성숙한 모델링을 갖춘 기존 사업은 고학력의 전문 인력이 계속 최적화해야 하는데, 현실적으로 그 수요를 따라갈 수 없다는 걸 알고 있음. 그래서 모델링이 구조화되지 않은 곳을 찾지만, 거기서도 이 접근을 쓸 수 있을지는 모르겠음

Jane Street의 관점에서 봐야 함. 그들은 고빈도 거래 회사이고 주식과 금융상품을 수백만, 어쩌면 수천만 단위로 거래함
거기에는 “고치면 된다”가 없음. 무엇이 잘못됐는지 이해할 때쯤이면 이미 수십억을 잃었을 수 있음
그래서 공격적 방식은 비핵심 영역에서는 통할 수 있음
참고로 이미 곳곳에서 방어적 방식을 쓰고 있음. Python, Java 등에는 가비지 컬렉터가 있고, 코드가 의도대로 실행된다는 점이 검증되는 셈임
언제쯤 형식 검증이 보이기 시작할지 궁금했는데, 구현 세부사항을 걱정하는 단계에서 문제를 과학적·수학적으로 서술하는 단계로 가는 건 자연스러움

“공격적 프로그래밍”이라는 표현이 좋음. 다만 그 패러다임은 이미 업계의 기본 상태임
Gen AI 때문에 방어적 프로그래밍의 비용은 크게 내려갔고, 인간 검증의 비용은 크게 올라갔음. 반면 형식 기법은 검증을 싸게 만들지만, 명세·타입·증명을 쓰고 구현을 단단한 틀에 맞춰 구부리는 등 구현 오버헤드가 큼
그런데 Gen AI가 그 힘든 작업을 자동화할 수 있음. 둘은 천생연분임

번역되지 않은 영어 문서를 기계번역에 의존한다면, 주제와는 조금 벗어나지만 영어를 배우는 것을 강하게 추천함
약간의 노력이 필요하지만, 계속되는 번역 오버헤드를 없애면 엄청난 도움이 될 것임

이런 방법론이 사치라는 데 동의함. 글에서도 그 점을 인정하고 있고, Jane Street는 이 접근에서 이익을 얻기에 꽤 특수하게 준비된 조직임

Jane Street가 자신들에게 관련 있어서 그런 글을 낸 건 당연하고, 모든 프로그래밍에 일반적으로 적용되지 않는 것도 당연함
다만 스스로를 “사회적 패배자”라고 하거나 커리어에서 이런 실천을 따르지 않는다는 점이 이 논점과 어떻게 관련되는지는 잘 모르겠음

최근 관련 아이디어를 가지고 놀고 있는데, 놀라웠던 건 최전선 모델, 특히 ChatGPT-5.5가 Roqc, 예전 Coq 증명 보조기에서 특정 수동 증명을 얼마나 잘 완성하느냐였음
증명이 항상 예쁘진 않지만, ChatGPT는 제한적이지만 0은 아닌 증명 보조기 경험과 증명되는 보조정리 분야의 꽤 큰 도메인 경험을 가진 내가 훨씬 오래 걸릴 일을 몇 분, 10~100회 반복 안에 증명하는 경우가 많음
이 짧은 글의 맥락에서 이게 흥미로운 이유는 특정 형식 기법 도구가 동작하는 기본 가정을 흔들기 때문임. Frama-C, Ada/SPARK 등은 CVC5, Z3 같은 도구가 자동으로 해소할 수 있는 증명 의무를 생성하는 데 집중하고, 실패하면 Roqc에서 수동 증명하는 꽤 고통스러운 대안으로 넘어감
흔한 흐름은 어떤 의무가 “어렵다”, 즉 자동으로 해소되지 않는다는 걸 발견한 뒤, 코드의 의무 생성 지점에서 보이는 보조정리와 단언 집합을 재구성해 “쉽게” 만들거나, 심지어 코드를 바꾸는 것임
Roqc 증명이 두 배로 비싼 세계에서는 말이 됨. 사람에게 작성이 어렵고, 코드와 주변 증명이 변할 때 유지보수 변동도 크기 때문임
하지만 Roqc 증명이 “AI가 루프에 들어간 자동 해소”가 된다면 이 비용 차이가 사라짐. 그러면 증명을 코드처럼 쓸 수 있고, 사람이 읽기 쉬운 명료함을 1순위로, 컴파일러나 증명기 최적화는 한참 뒤로 둘 수 있음. 그 함의는 아직 완전히 소화하지 못했지만 꽤 흥미로움

요구사항이 바뀌어서 증명할 수 없는 상황에서, AI가 증명을 쉽게 만들려고 코드와 요구사항을 바꿔버릴 가능성은 얼마나 될까
증명은 다뤄본 적 없지만, “변경 후 이 테스트가 실패했다”고 말하면 AI가 내 의도인 기존 테스트와 새 테스트를 모두 통과하도록 코드를 고치는 대신 테스트 자체를 바꿔버리는 일은 가끔 봤음

내 경험과 비슷하지만, 나는 Lean을 골랐음. 만들고 싶던 기능과 더 관련이 컸음
앞으로가 기대됨

ChatGPT가 Roqc 증명을 몇 분과 10~100회 반복 안에 해낸다고 할 때, 그 증명 자체가 올바른지는 어떻게 아는지 궁금함

형식 명세 이야기를 읽을 때마다 “같은 테스트를 다른 방식으로 쓰는 것”처럼 보이고, 더 나쁘게는 “같은 구현을 다른 방식으로 쓰는 것”처럼 보임
두 번 작성하면 오류를 잡는 데 도움이 될 수는 있겠지만, 형식 명세도 테스트나 구현과 똑같은 버그를 가질 수 있다면 무엇이 특별한지 잘 모르겠음
근본 문제는 프로그램이 뭔가를 한다는 걸 형식적으로 증명하려면 그 “뭔가”를 매우 구체적으로 정의해야 한다는 데 있음. 그러면 사실상 테스트나 구현을 다시 쓰는 것처럼 됨
몇 년 동안 이 주제를 간헐적으로 들여다봤고, 뭔가 놓치고 있다는 느낌이 계속 드는데 그게 뭔지 모르겠음. 누가 설명해줄 수 있을까

Dijkstra의 유명한 말처럼, “프로그램 테스트는 버그의 존재를 보일 수는 있지만, 부재를 보일 수는 없다”
테스트의 결함은 문제가 될 수 있다고 생각한 동작만 테스트할 수 있다는 점임. 잘못될 수 있다는 걸 몰랐던 동작까지 선제적으로 고치려면 도구상자의 더 특이한 도구가 필요함. 퍼즈 테스트가 그 방향의 한 시작이고, 형식 검증도 또 다른 시작임
물론 이런 도구의 품질은 원하는 동작은 허용하고 원하지 않는 동작은 금지하는 포괄적인 형식 모델을 얼마나 잘 쓰느냐에 달려 있고, 여러 분야에서 우리는 여전히 놀랄 만큼 그 지점에서 멀리 있음

큰 차이는 형식 기법이 모든 것에 대해라는 전칭 한정자를 쓸 수 있게 해준다는 점임
예를 들어 단위 테스트에서는 “foo('abc')가 뒤쪽 공백이 없는 문자열을 반환한다”고 쓸 수 있음
하지만 형식 기법으로는 “임의의 입력 x에 대해 foo(x)가 뒤쪽 공백이 없는 문자열을 반환한다”고 증명할 수 있음
사소한 예지만, “임의의 프로그램 P에 대해 compile(P)는 P와 같은 동작을 한다” 같은 더 복잡한 것도 상상할 수 있음
물론 “같은 동작”이 무엇인지는 정의해야 함

소프트웨어는 안 쓰지만 ASIC과 FPGA 설계에서는 형식 기법 명세가 SAT 솔버 같은 도구를 써서 대상 설계가 명세를 만족하는지 판단하게 해줌
설계의 속성을 지정하면 도구가 다양한 방식으로 설계를 테스트해 그 속성을 위반할 수 있는지 확인함
예를 들어 교통 신호를 제어하는 시스템이라면, 서로 교차하는 차선이 동시에 또는 일정 시간 안에 둘 다 초록불이 될 수 없다는 속성을 지정할 수 있음
도구는 이를 완전 탐색으로 확인하고, 위반하는 코드 추적을 보여줄 수 있음

단순히 “같은 테스트를 다른 방식으로 쓰는 것” 이상임. 각 테스트는 대체로 독립적이거나 관리 불가능하게 커지고, 테스트 묶음의 완전성을 분기 커버리지 같은 비교적 거친 겹침 방식으로 따져야 함
정적으로 증명되는 타입 시스템은 각 구성 요소가 다른 모든 요소와 미리 맞춰 검사되도록 해줌. 단순히 “이 테스트가 통과한다”가 아니라, 조합했을 때 “이 모든 테스트가 합리적이고 일관된 전체를 만든다”를 보장하고, 일관되지 않은 모델이 코드에 구현되는 것을 막음
Rust의 match가 가능한 모든 분기를 완전히 다루도록 요구하는 것을 코드베이스 전체 규모로 확대한 예와 비슷함
근본적인 논리나 이론 오류를 만들면 잡아주지 못한다는 점은 맞음. 하지만 예컨대 Haskell 타입 시스템, 임시 함수형 테스트, 속성 테스트를 합친 것보다 훨씬 견고하다는 데 놀랄 수 있음. 그것도 전체적으로는 강한 체계라고 보지만, 형식적으로 증명된 암호학은 훨씬 높은 기준임

강력한 차이는 특정 테스트와 전수 증명 사이에 있음. 경계 조건 테스트를 떠올리지 못하면 그대로 놓침. 좋은 모델이 있으면 배포 전에 그 존재를 알고 고칠 수 있음
특히 동시성·분산·다중 스레드 상황에서 가치가 큼. 경쟁 조건과 교착 상태는 테스트하고 추론하기 매우 어렵고, “A, B, C가 A, C, B 순서로 일어날 수 있는가” 같은 문제가 그렇음
이 분야의 성숙은 대략 이렇게 갈 것 같음. 첫째, LLM이 처음에는 “두 번째로 해보기”식 사후 검증에 그치더라도 형식 기법의 학습과 사용을 훨씬 빠르게 할 것임
둘째, “구현 코드가 바뀌었는데 모델을 깨뜨린 것처럼 보이나?”를 LLM이 확인하는 자동화로 이동할 것임. 여전히 결정적이지는 않지만, 가끔만 바뀌는 무언가를 사람이 리뷰해야 하는 것보다는 훨씬 나을 가능성이 큼
셋째, 진짜 도약은 “형식 명세만 쓰고 구현은 생성하라”는 도구를 다음 단계로 끌어올리는 데 있을 것임. 이런 코드 생성 프로젝트는 이미 여럿 있지만 대부분 회사들이 원하는 수준까지 완전히 익지 않았음. LLM 도구가 그중 하나를 필요에 맞추는 데 드는 1~2년의 수작업을 가속할 수 있다면 어떨까

Kleppmann의 이전 글 https://martin.kleppmann.com/2025/12/08/ai-formal-verificati...도 참고할 만하고, 타입 시스템이나 린터에 넣을 수 있는 것은 당연히 그렇게 할지 저울질해야 함
더 쓰기 편한 방식이 나오길 바람. 글에 나온 도구 중에는 dafny와 iris가 산업용에 가장 가까운 듯함. Amazon S3도 내부에서 TLA를 써온 이력이 있는 것으로 앎
하지만 이 분야의 TypeScript 같은 존재, 기존 도구에 자연스럽게 들어가고 비용 없는 추상화처럼 작동하며 사람들이 진심으로 예전 방식보다 선호하는 무언가는 아직 못 본 것 같음
커스텀 린터를 쓰는 것도 여전히 꽤 별로임. golangci-lint는 고통스러운 코드베이스이고, semgrep은 안 써봤지만 규칙 엔진이 위압적으로 보였음. 마음에 드는 AST API도 아직 못 써봄

연역적 추론, 즉 “형식 기법”에 대한 이런 찬가는 늘 그 근본 한계를 빠뜨림. 공리와 정의가 대상 도메인에 얼마나 잘 맞는가라는 문제임
“이론상 이론과 실제는 차이가 없다. 실제로는…”이라는 말과 같음. Jane Street는 코드의 목적이 결정적 알고리즘을 구현하는 것이라 매핑이 1:1인 큰 코드베이스를 유지할 것이라고 추측함. 많은 개발자가 그런 영역에서 일하지만, 수백만 명은 그렇지 않음. 대부분의 UI, 대부분의 탐색적 작업 등이 그렇음
형식 기법과 나란히, 논리·수학적 방식은 아니지만 승인 기준을 높은 해상도로 정의하려는 흐름도 있음. 이 흐름은 적어도 매핑 문제와 씨름하지만, 지도가 영토가 아닌 대부분의 곳에서는 해결하지 못함
Google 검색 결과 페이지는 극도로 진화한 내부 최적화 프레임워크를 갖췄지만 정말 최적점에 도달했을까? 흐릿한 아이디어를 잡으려고 급히 만든 프로토타입이 더 잘 보여줄 수도 있었을까? 이런 질문은 시스템 내부가 아니라 그 시스템이 섬기는 바깥을 보아야 가장 잘 답할 수 있음

형식 기법은 정확히 의미론이 잘 정의된 도메인을 위한 것임
논리 회로, 형식 검증이 많이 들어가는 CPU 구성요소, 커널, 프로토콜, 파서, 컴파일러, 암호학, 보안 프레임워크, 동시성 기본 요소 등은 검증에서 큰 이익을 얻음

Google 결과 페이지 자체는 잘 정의되어 있지 않지만, 그 아래 코드의 아마 90% 이상은 잘 정의되어 있을 것임
그리고 어떤 경우에는 결과가 잘 정의되어 있지 않아도 학습할 수 있으므로, 무엇이 말이 될지 앉아서 생각하는 문제만은 아님

프로그래밍 언어의 설계와 구현에 조금 관심 있는 입장에서 이 문장이 정말 흥미로웠음. “프로그래밍 언어를 다루는 대부분의 사람에게 쉬운 부분은 프로그래밍을 더 좋게 만들 새롭고 더 나은 아이디어를 내는 것이다. 어려운 부분은 누군가가 그 아이디어를 실제 일에 쓰도록 설득하는 것이다”
완전히 동의함. 이득이 있더라도 새 언어에 넣을 수 있는 낯섦의 양에는 한계가 있음
하지만 AI 에이전트는 프로그래밍 언어 설계의 급진적으로 새로운 아이디어에 큰 저항을 느끼지 않을 것임. 에이전트형 AI 이후 프로그래밍 언어 설계가 어떻게 진화할지 한동안 생각해왔음
채택 걱정을 훨씬 덜 할 수 있을 때, 프로그래밍 언어를 개선하기 위해 어떤 새 아이디어를 만들 수 있을지 보는 것은 매우 흥미로울 것 같음 https://steveklabnik.com/writing/the-language-strangeness-bu...

애플리케이션 보안 테스트 쪽에서 형식 기법을 적용하는 방향으로 작업 중이고, 같은 접근을 비즈니스 로직 검증에도 적용할 수 있다고 봄
이를 위해 taint analysis를 쓰고 있음. 꽤 잘 확립된 형식 기법 접근이지만, 실제 코드베이스의 데이터 흐름 복잡성 때문에 현장에서는 아직 널리 적용되지 않았음
형식 기법을 AST 패턴 매칭과 단순한 타입 검사 너머로 확장하는 건 정말 어려운 작업임. taint analysis로 실제 코드베이스의 절차 간 데이터 흐름을 몇 분 안에 추적하고 깊이 숨은 취약점을 찾는 수준에 도달하기까지 수년의 연구개발이 걸렸음
관심 있으면 프로젝트를 볼 수 있음: https://github.com/seqra/opentaint

약 18개월 전에 LLM과 함께 타입을 쓰는 데 빠졌고, lean4에 진지해진 건 6~8개월 전쯤임. 이제는 실용적인 C/C++ FFI, 따라서 사실상 모든 것과 연결되는 CIC 증명 기반 없이는 소프트웨어 작업에 AI 보조를 쓰는 걸 고려하지도 않음
JSON부터 Python까지 모두 금지했고, nix도 컴파일러가 있도록 다시 썼음. 우리가 쓰는 거의 모든 것은 속성 테스트와 여러 퍼즈 테스트를 한계까지 거칠 뿐 아니라, 최소한 .olean 연결을 통해 속성 테스트를 구동하는 lean4 증명을 갖고 있음. 여유가 있으면 도메인 전체의 완전성까지 증명하고 그 속성도 테스트함
빠른 부분은 모두 lean4에서 생성되므로 C++/Rust 논쟁은 건너뜀. C++의 버그가 실제로는 lean4 코드의 버그일 때 장점이 있지만, 어느 쪽으로도 갈 수 있음
큰 변화이고, “JSON과 Python을 금지한다고?”라며 회의적인 사람을 탓하지는 않음. 하지만 우리는 이런 방식으로 수백만 줄을 검사했고, AI + 형식 시스템은 AI 없음에서 AI와 Python으로 가는 것보다 훨씬 더 큰 도약임. 후자는 우리의 경험상 진전이 단조롭지 않지만, 전자는 거의 항상 단조롭게 나아감
꽤 과감한 일도 가능함. 이것은 ISL과 CuTe 같은 것들이 모델링하는 다면체 텐서 계산의 형식 증명이고, 이를 이용하면 C++23의 mdspan으로 장치에서 swizzling과 tiling을 하고 그것이 맞다는 것도 증명할 수 있음. 다만 이 예시는 커버리지에 대한 L'Hopital식 논증을 잘 보여주지는 않음: https://github.com/b7r6/mdspan-cute
그 결과는 정말 빠르고, 첫 시도부터 빠름 https://straylight.software/assets/lambda-hierarchy.svg