[Bongjun] add pldi25 post

Author: bongjunj

_posts/2025-06-28-bongjun-pldi25.md

@@ -0,0 +1,183 @@
+---
+title:  PLDI 2025 여행기
+date:   2025-06-28
+author: Bongjun Jang
+kor_author: 장봉준
+tags:
+  - Trip
+  - PLDI2025
+classes: wide
+---
+
+| ![](https://lh3.googleusercontent.com/pw/AP1GczOdSxOrUDke-m1pvLlHTAWigf9OMRLwVWYpzt3rffyrpS0TNgN91zdWV1avlo5uQMpua3S7SVv6uUvmOO4chb-EJPzGLXK5OTbTrZmn8rDvv6tbLWPmADxeLuKo3VNtFXmUD_pDpwY8L0UeoqEXdIY-=w1261-h1683-s-no-gm?authuser=1) |
+| :-: |
+|<b> 학회장과 광화문이 가까워 밤에 뛰러 나가는 겸 구경갈 수 있었다 </b>|
+
+PLDI 2025는 태어나 처음으로 참가하는 국제학회였다.
+그 중에서도 세계 최고 프로그래밍 언어 학회 PLDI가 우리나라 서울에서 열린 점이 아주 특별했다.
+전세계 연구자들이 우리나라로 찾아오고, 거기다 내 연구를 우리나라에서 발표하기도 했으니 이보다 멋진 경험을 찾기는 힘들 것 같다.
+
+전세계에서 모인 빼어난 학생들과 연구자들을 만나 이야기하며 연구 아이디어 이야기로 동기를 부여받기도 하고,
+연구하며 어려웠던 점이나 사람 사는 이야기를 하면서 같은 커뮤니티의 일원으로 동질감을 느끼기도 하였다.
+이 기행문을 통해 PLDI 2025 5일간 나의 경험을 공유해보고자 한다.
+
+## PLDI 워크샵
+
+PLDI 첫 2일은 워크샵으로 시작했다.
+그 중에서 첫날 오전에는 egglog 튜토리얼에, 오후에는 PLMW이 열려 참석하였다.
+
+### egglog 튜토리얼
+
+egglog는 equality saturation 워크로드를 위해 구현된 egg(https://github.com/egraphs-good/egg)와 Datalog를 통합한 프레임워크다.
+equality saturation은 나의 관심 분야인 컴파일러 최적화에서 최근 많은 관심을 끌고 있는 기술이다.
+예를 들어, 최근 등장한 Cranelift 컴파일러(https://github.com/bytecodealliance/wasmtime/tree/main/cranelift) 는 e-graph를 사용해 컴파일러 최적화기와 코드 생성기를 구현해 컴파일러 구현에 새로운 방향을 제시하고 있다.
+튜토리얼에서는 egglog를 이용해 추론 규칙(Inference Rule, Deductive Reasoning)과 재작성 규칙(Rewrite Rule)을 선언하고 이를 통해 간단한 프로그램 분석기를 구현하는 방법, 코드 최적화기를 구현하는 법을 다뤘다.
+튜토리얼의 자세한 내용은 https://github.com/[egraphs-good/egglog-tutorial](https://github.com/egraphs-good/egglog-tutorial)에서 확인할 수 있다.
+
+튜토리얼을 통해 e-graph가 정말 흥미로운 연구대상임을 다시 느꼈다.
+컴파일러 최적화기를 만들어낼 수도 있고, 프로그램 분석기를 만들어낼 수도 있다.
+e-graph의 적용 분야는 자동증명기, 프로그램 합성기, 그리고 새로운 재작성 규칙 발견(https://dl.acm.org/doi/10.1145/3485496)까지도 나아가고 있다.
+지금 내가 하고 있는 컴파일러 최적화 연구도 어떻게 e-graph의 지평을 넓힐 수 있을지 기대된다.
+
+### PLMW
+
+첫날 오후에는 PLMW에 참석하였다. PLMW는 멘토링 워크샵으로 워크샵 양일 모두 열렸는데,
+나는 그중에서도 첫날 서로 얼굴과 이름을 익히고 가까워질 수 있는 자리에 참석하였다.
+
+특히 PL Card 프로그램에서 재밌는 기억이 많다. 이 프로그램은 카드 뭉치에서 카드를 뽑아 적혀있는 제시어를 설명하는 퀴즈 게임이다.
+카드에 금지어도 적혀있었는데 금지어를 말하지 않고 제시어를 설명하는 게 꽤 고역이었다.
+예를 들어, "C++" 제시어를 설명하려고 하는데 "C"나 "Programming", "Language" 처럼 당연히 떠오르는 단어를 말하지 않고 "C++"을 제한시간 안에 설명하려고 하니 꽤 난이도가 있었다.
+Constrained Decoding이 걸려 토큰 확률 분포가 고장난 언어모델이 된 기분이었다.
+"C++"에 대한 나의 설명은 "Rust wants to get rid of it"이었는데, 같은 테이블에 있던 누군가 바로 맞췄던 기억이 난다.
+
+또, "Garbage Collection"도 문제로 나와 나는 "C++은 이게 없는데 Java에는 있어"라고 설명했었다.
+그런데 퀴즈가 끝나고 누군가 C++ standard에 Garbage Collection이 있지만 이를 따르는 C++ 구현체가 없다는 설명을 해줬다.
+정말로 찾아보니 C++ 스탠다드에 Garbage Collection이 있었다.
+도대체 C++에 없는 기능은 무엇이고, 그리고 이런 사실을 어떻게 아는 것일까.
+프로그래밍 언어 고수들의 세계에 왔다는 생각이 들었다.
+
+PLMW 세션을 통해 포르투갈에서 컴파일러를 연구하고 있는 Lucian과 친해졌는데
+내가 매일같이 사용하는 Alive2를 개발한 Nuno Lopez 교수님에게 지도를 받는 학생이었다.
+Lucian은 마지막 날 내 발표에 찾아와 질문을 하기도 했고, PLDI 5일간 종종 만나 좋은 대화도 많이 나눴다.
+
+![](https://lh3.googleusercontent.com/pw/AP1GczNhcKTuAuojNryZCig6UlcH1JnBYBLnofUP55C4AgGNWol6dej-MeOXNZJkWFmGY4H35lC4IdNg2tAZ-zdo7fAb0-mcMeripEP0G7zvTL5VWSWh2uom9Z5V5zolRHOEVzU9VC7pl3gp1KURwzJoCUFN=w2048-h1536-s-no-gm?authuser=3)
+
+PL 연구에 HCI의 원리를 적용하는 법에 대한 발표도 흥미로웠다.
+연단이 아니라 무대 중간으로 나와 발표 내내 청중의 흥미를 끌어내는 발표 방식도 인상적이었다.
+HCI의 사용자 연구는 사용자가 겪는 문제를 이해하고, 문제에 대한 해결책을 디자인하고, 해결책의 효과를 입증하는 과정을 거친다.
+사용자들이 겪는 문제를 사용자들이 원하는 해결책으로 해결가능한 경우가 많지 않기 때문에 문제를 제대로 이해하는 것이 중요하다는 것에 공감하며 강연을 들었다.
+PL과 HCI는 서로 거리가 먼 분야로 여겨지는데, 이 두 분야를 결합하는 아이디어가 있다는 것이 놀라웠다.
+
+### RPLS (Real-World Programming Language Specification)
+
+둘째날 열린 RPLS에서 오전 세션이 특히 재미있었다.
+그 중에서도 인터프리터, 컴파일러, 번역검산기 등 PL 도구를 자동으로 생성해내는 K-Framework 연구가 기억에 남는다.
+
+K-Framework (이하 K) 발표는 제목부터 강력했다.
+["Programming Languages Must Have Formal Semantics. Period."](https://pldi25.sigplan.org/details/rpls-2025-papers/2/Programming-Languages-Must-Have-Formal-Semantics-Period-).
+발표가 끝나고 연사인 Xiaohong Chen과 커피를 마시며 K에 대해 심도 있는 설명을 들을 수 있었다.
+그 중에서 K의 설계 철학 그리고 올바름(Correctness)에 대한 설명이 기억에 남는다.
+
+먼저, K는 연구 프로젝트로 시작했지만 이론보다 사용성에 더 무게를 두고 설계했다는 점이 흥미로웠다.
+아무리 강력한 이론도 실제 세계에서 외면 받는다면 큰 족적을 남길 수 없는 게 사실이다.
+그래서 K는 프로그래밍 언어 개발자들이 사용할 수 있는 도구들 즉 인터프리터, 컴파일러, 번역검산기 등을 자동으로 생성하고 바로 사용할 수 있도록 기능적인 측면을 강조하며 개발되었다고 한다.
+
+또한, 올바름은 우리가 "무엇을 믿어야하는가"를 잘 따져봐야 논의할 수 있는 것이기 때문에 조심스럽게 접근해야한다는 설명도 들었다.
+만약에 Z3 기반의 번역검산기를 사용한다고 해보자. 이 번역검산기의 결과를 그대로 사용한다면 우리는 Z3가 사용하는 논리 기반을 그대로 믿는 것이 된다.
+하지만 정말로 그 논리 기반을 믿을 수 있는가? 게다가 Z3의 구현이나 번역검산기의 구현에 헛점은 없는가?
+이는 수학에서 어떤 공리계를 믿어야 하는지를 의심하는 것과 비슷해 보였다. (참고: [수학의 선택공리 논쟁](https://en.wikipedia.org/wiki/Axiom_of_choice#Criticism_and_acceptance))
+
+이런 점으로 미루어 볼 때, 거대한 K를 어떻게 그대로 믿을 수 있을까?
+만약 K에 버그가 있다면 K가 만들어내는 모든 도구들도 신뢰할 수 없게 된다.
+그래서 K는 K가 하는 모든 것에 자동으로 증명을 생성한다. 모든 것을 신뢰하지 않고 증명한다. 증명에 사용되는 공리도 매우 적어서 신뢰 문제에서 더 자유로울 수 있다는 설명이었다. 신뢰해야 하는 것이 적어서 더 신뢰할 수 있는 시스템이라는 설명이 재미있었다.
+
+
+## 기억에 남는 발표들
+
+### [Program Synthesis from Partial Traces](https://dl.acm.org/doi/abs/10.1145/3729316)
+
+![](https://lh3.googleusercontent.com/pw/AP1GczM-dFAxelPAMF4H1ydieRfvVp8n5VLlRqyGha8aqtWoZatb9CAYjREb_QK_1sZCfQNaUujiYF7Gqdm4I6AjVpkyBdFFpge6lXsfGuHLCzNoT89DKPsqHKcOJoq4UI-F3Z2QUiQiG8mRXVF-qjvqGcNa=w2048-h1536-s-no-gm?authuser=3)
+
+PLDI 본행사 첫째날 프로그램 합성(Program Synthesis) 세션에서 발표된 논문이었다.
+발표 흐름에 맞춰 자연스럽게 진행되는 슬라이드 흐름과, 잘 정리된 내용이 독보적인 발표였다.
+AWS 연구 인턴으로 진행된 프로젝트였는데, 클라우드 서비스를 사용할 때 남는 API 로그(Partial Traces)를 통해
+사용자가 자주 반복하는 일들을 원클릭으로 한번에 실행할 수 있는 프로그램으로 만들어주는 것이 아이디어다.
+예를 들어, 가상머신 인스턴스를 종료하고, 종료되지 않았다면, 강제로 종료하는 것을 사용자가 반복해 이것이 로그로 남는다면
+이 전체 과정을 사용자가 원클릭으로 다시 사용할 수 있는 프로그램으로 만들어주는 것이다.
+
+질문 시간에 정보보호개론 조교를 하며 가상머신 150개를 세팅하던 경험이 떠올라 내 경우에도 사용할 수 있는지 물어봤다. ("This is exactly the tool I need!")
+프로그램 로그만 잘남고, 내가 하는 일들이 API 단위로 잘 정리되어 있다면 안될 이유는 없다는 답을 들었다.
+발표가 끝나고 나서 복도에서 만나 더 얘기를 했는데, 가상 머신이 모종의 이유로 작동을 멈추는 경우, 모든 가상머신을 한번에 세팅하면 안되는 이유 등 여러 엣지 케이스들에 대해 같이 생각을 해봤는데 재미있는 결론이 났다.
+만약 조교 업무를 1년마다 반복하게 된다면, 해가 갈수록 엣지 케이스를 더 잘 해결하는 프로그램을 합성하게 될 것이다.
+그런데 이전에 합성해둔 프로그램을 이용해 새로운 케이스에 대해 더 잘하는 프로그램은 어떻게 만들 것인지 잘 알려진 방법이 없는 것이다. 이 방법을 찾으면 아마 박사학위를 하나 더 받을 수 있겠다고 농담하며 이야기는 일단락되었다.
+
+### Lean
+
+둘째날 기조연설과 Industry 세션에서 모두 Lean에 관한 이야기가 나왔다.
+예전 NYU 부전공 프로그램에서 프로그램 검증 수업을 청강했던 경험이 내용을 이해하는 데 많은 도움이 되었다.
+NYU에서는 Rocq(그 당시에는 Coq이라 불렀다)를 사용했었는데, 비슷한 시스템인 Lean이 최근 이렇게까지 성장했다는 사실이 놀라웠다.
+
+아침 기조연설에서는 Lean의 창시자, Leonardo de Moura가 Lean의 여러 면모를 설명했다.
+최근 테렌스 타오가 Lean을 적극적으로 사용하는 모습을 보여주면서 많은 관심을 끌고 있다는 것은 알았지만 기조연설을 통해 몰랐던 사실을 더 많이 배울 수 있었다.
+특히나 Lean을 증명보조기 종류 중 하나로만 생각했었는데 자동증명기와 일반적인 프로그래밍 환경까지 통합되어 여러 분야에 사용될 가능성이 많아보였다. 최근 내가 하고있는 컴파일러 최적화 검증을 자동화하는 데에도 도움이 되지 않을까 생각했다.
+
+오후 Industry 세션에서는 AWS 공순호 박사님이 Lean을 이용해 AI를 훈련시키는 연구 방향에 대해 이야기해주셨다.
+잘 해결되지 않는 어려운 문제에 대해 LLM이 사실상 동전던지기보다 나은 점이 없다는 위트있는 시작과 함께 강연이 시작되었다.
+강연은 AI를 훈련시킬 데이터가 고갈되어가는 세상에서 Lean과 같이 엄밀한 시스템이 새로운 데이터를 합성시키는 역할을 할 수 있다는 것이 핵심이었다. 또한 AI가 Lean과 상호작용하며 강화학습을 통해 성능을 향상시킬 수 있다는 점도 재미있는 연구방향이었다.
+
+PLDI가 끝나고 Lean을 더 공부해보기 위해 Lean의 기반인 Dependent Type Theory도 간략하게 공부해보고,
+테렌스 타오가 공개한 Lean으로 작성된 해석학 교재를 따라가보며 증명도 작성해보았다.
+아직 내가 이걸 사용해서 어떤 일을 할 수 있을지 감은 안오지만 Lean이 저변을 계속 넓혀가고 있는 만큼
+언젠가 다시 Lean을 만날 날이 오지 않을까 생각이 들었다.
+
+## 연구 발표
+
+![](https://lh3.googleusercontent.com/pw/AP1GczM1EZGu0es55xxyxvZBNWS6qNSvrqeCsBKe4chBpznhkqUwgGpD663VvsD76lY1Z7qQDX-ZqSxIU6ZG9QlTFAT8BWgdG-pvN5l5HU_3BZ6AD0uQMqh8p4OSh8_i2sN1Jb87T5CMO3ntaf5ra3XGwlpA=w2048-h1536-s-no-gm?authuser=1)
+
+나는 PLDI 본행사 마지막날 오전 컴파일러 세션에서 발표하게 되었다.
+태어나 처음으로 하는 학회 연구발표가 PLDI라니 정말 뜻깊고 신기한 경험을 했다.
+첫 발표, 그리고 PLDI 발표이니 만큼 15분안에 연구 결과의 핵심을 뚜렷하게 전달하기 위해 많은 노력을 했다.
+설명은 최대한 단순명료하게 다듬고, 연구의 배경이나 개념이 생소할 경우를 대비해 오해가 없도록 내용을 준비했다.
+그리고 관중이 압도되지 않도록 애니메이션을 통해 한번에 하나씩만 설명하도록 발표 내용을 준비했다.
+연구실 리허설에서 교수님과 다른 분들이 슬라이드의 작은 점 하나하나, 그리고 발표 흐름의 오류까지 꼼꼼하게 찾아주신 덕분에 가능했다.
+
+발표 전날에 마지막 점검을 했다. 호텔에서 치맥을 시켜놓고 태은님, 수진님, 그리고 동재님이 발표를 다시 한번 점검해주셨다.
+마지막 점검이었는데 내 입, 슬라이드 애니메이션 그리고 몸짓이 동기화된 것을 확인하니 기분좋은 자신감이 솟아났다.
+긴장한탓에 말을 빨리 해서 주어진 15분보다 시간을 덜 쓰긴 했지만
+다음날 무대에서는 이것만 조심하면 되겠다고 다짐하며 치맥과 함께 마지막 발표 준비를 마쳤다.
+
+PLDI 본행사 마지막날 11:50에 발표를 시작했다.
+슬라이드 애니메이션을 모두 머리에 외우고 무대 가운대로 와서 설명할 생각이었는데 (스티브 잡스처럼 하고 싶었다),
+생각과 다르게 프로젝터 빔이 내 눈에 닿는 바람에 옆으로 비켜 설명해야했다.
+무대 구조가 예상과 달라 조금 당황하긴 했지만 전날 밤 리허설을 상기시키며 15분을 최대한 모두 사용하려고 주의하며 발표를 진행했다.
+발표 도중 연구에 관심을 가져주신 분들이 슬라이드 내용을 사진으로 찍어가는 경우도 볼 수 있었고,
+발표를 마치고 남은 시간에 질문도 여러번 받았다.
+세션을 모두 마치고 추가적인 질문도 받아서 준비한 내용을 성공적으로 전달한 것 같아 많은 보람을 느낄 수 있었다.
+연구실 내부 리허설, 전날 점검 그리고 발표 당일까지 격려과 많은 관심을 보내주신 연구실 분들께 감사하다는 말을 전하고 싶다.
+
+## 네트워킹 경험
+
+
+| ![](https://lh3.googleusercontent.com/pw/AP1GczMhxPZ_lekK0SOuh9cUPyYeafTXBy2WmWm2Nvmh7-xFUm_GF2pPPcwxDhsHu1_hfNZyDxEW4x3r90rbVSMUkYPOKDitgjbNjwAgO9dVriD7yJmi1EqSZCEtPktAFH4vsGLwQGowQz0EGR-zXS8e38uS=w2048-h1536-s-no-gm?authuser=3) |
+| :-: |
+|<b> 컴파일러 세션에서 발표중인 Chris Fallin </b>|
+
+이번 PLDI 2025에서 다른 연구자들과 네트워킹한 경험도 빼놓을 수 없다.
+
+최근 연구하고 있는 Cranelift 컴파일러의 리드 개발자인 Chris Fallin, Cranelift 컴파일러의 최적화 규칙과 코드 생성 규칙의 검증 도구 [Crocus](https://dl.acm.org/doi/10.1145/3617232.3624862)를 작성한 Alexa VanHattum도 만나 얘기할 수 있었다. 최근 Cranelift에 최적화 규칙을 추가하는 PR을 4개 보냈었는데 Chris Fallin이 나를 알아보는 신기한 경험도 하고, 내 연구 방향에 대해 설명하는 기회도 가졌다. 내 연구를 알아보는 사람들이 있다는 걸 느끼고, 사람들에게 도움을 줄 수 있는 연구를 더 열심히 해야겠다는 다짐을 했다.
+
+우연히 Lean의 창시자 Leonardo de Moura와 옆자리에 서게 되어 Lean 개발 이야기도 생생하게 들을 수 있었다.
+또한, 내가 자주 사용하는 [Alive2](https://github.com/AliveToolkit/alive2)의 창시자인 Nuno Lopez도 만나 얘기해볼 수 있었는데, 스마트폰없이 피처폰만으로 서울을 돌아다니는 무용담을 들을 수 있었다. (생각해보니 같이 사진이라도 찍을 걸 그랬다!)
+
+또한 우리나라에서 PL을 연구하시는 다른 분들도 만나는 기회도 가졌다.
+연세대학교 정기웅 박사과정님의 소개로 고려대학교 전민석 박사님, 우리학교 강지훈 교수님 연구실의 안해찬님, 이정인님을 만나 같이 식사자리를 가졌다.
+이와 더불어 서울대학교 연구실에 계시는 대학원생분들은 어떤 분야에 관심을 가지고 계시는지도 알 수 있었다.
+우리나라에서 정형검증에 관심을 가진 분들이 많이 있다는 것을 느꼈고, 시간이 날 때마다 나도 전산논리를 다시 공부하고 Lean을 익혀야겠다는 생각을 했다.
+
+## 마치며
+
+이번 PLDI 2025는 다른 연구자들과 만나 내 시야를 넓히고 재미있는 아이디어들을 배울 수 있었던 최고의 학회였다.
+최대한 많이 배워가고자 모든 세션에 적극적으로 참여하고자 했고 들은 모든 연구발표에 대해 최대한 질문을 하려고 노력했다.
+이런 학회에서 직접 발표까지 하다니, 정말로 영광스러운 기회였다.
+컴퓨터 과학자로서 한발짝 성장한 느낌이다.
+5일 모두 참여를 지원해주신 허기홍 교수님께 깊은 감사를 드린다.