TL;DR

  • 대형 언어 모델(LLM)이 코드를 잘 작성해 사람이 직접 코드를 쓰는 일이 줄더라도, 프로그래밍 언어(PL)의 아름다운 아이디어와 탐구 가치는 남아 있으며 더 큰 문제를 다룰 수 있게 됨.
  • 인공지능 도구가 프로그래밍에 미치는 영향으로 학계의 사기와 정신 건강이 악화되고, 일부 연구자는 분야의 실존적 위기를 느낌.
  • 연구의 동기를 노력이나 지능의 증명에서 탐험으로 옮기고, 응용이나 사용자 수에 얽매이지 말자는 주장임.
  • LLM을 활용해 인터프리터의 의미론을 생성·검증하고, 검증 도구를 에이전트에 맞게 조정하며, 새 언어의 의미론을 개발하는 실험이 진행 중임.
  • 증명 작성 자동화로 이론적 반사실 질문을 더 빠르게 검토할 수 있으며, 연구자는 자아보다 호기심과 탐험의 즐거움을 좇아야 한다는 제안임.

프로그래밍 언어 연구는 죽었음. 그래서 뭐가 문제인가?

  • TYPES 메일링 리스트에서 인공지능 도구가 프로그래밍 전반에 미치는 파괴적 영향과 연구 분야의 미래를 논의하는 스레드가 최근 열림.
  • 의견은 신중하게 제시됐지만 대체로 부정적이었으며, 일부 연구자는 실존적 위기를 겪는 상황임.
  • 한 참여자는 2026년 가을 학계 구성원의 사기와 동기가 1년 전보다 낮고, 스트레스와 불안이 높으며 정신 건강 위험도 커졌다는 경험적 관찰을 제시함. 그 영향은 코로나19 당시와 견줄 만하다는 평가임.
  • 이 글은 혼란스러운 시기에 진로를 정해야 하는 학생과 주니어 연구자에게 더 긍정적인 관점을 제시하려는 글임.
  • 연구 아이디어가 이보다 풍부했던 적이 없고, 새로운 문제가 매일 등장하며, 이전보다 훨씬 빠르게 질문을 던지고 답을 얻을 수 있다는 관점임.
  • 연구 공동체는 연구를 노력이나 지능의 증명으로 방어하는 자아 중심적 태도에서 벗어나, 처음부터 연구를 떠받쳐야 했던 더 고결한 동기인 탐험으로 옮겨가야 한다는 주장임.
  • 언어 모델은 코드를 매우 잘 작성하며, 그 결과 사람이 직접 코드를 작성하는 일은 점점 줄어들 전망임.
  • 이에 따라 사람은 프로그램을 작성하지 않을 텐데 프로그래밍 언어 연구가 쓸모없어지는 것 아니냐는 우려가 생길 수 있음.
  • 프로그래밍 언어 연구는 시작부터 이론과 응용 사이의 다리 역할을 맡아 왔으며, 연구자는 원칙에 기반한 우아한 아이디어를 다루면서도 그 결과가 결국 실용적 응용으로 이어지는 분야에서 일함.
  • 그러나 응용이 중요한지는 별개의 문제라는 도발적 관점임. 응용을 원했다면 소프트웨어 공학 분야에 있었을 것이며, 소프트웨어 공학 시스템은 임시방편적이고 조잡하며 불완전하고 간신히 작동하는 경우가 많지만, 리눅스 커널 전체를 처리하는 정적 분석기를 만들려면 우아함과 아름다움만 고집할 수 없다는 설명임.
  • 프로그래밍 언어의 아름다운 아이디어와 통찰은 여전히 존재하며, 이를 탐험하고 실험하고 즐길 수 있음. 대부분의 프로그래밍 언어는 개발자를 제외하면 사용자가 사실상 한 명도 없다는 주장임.
  • 사용자의 존재나 응용을 걱정하지 말고 프로그래밍 언어 연구를 하자는 도발적 제안이며, LLM을 활용하면 전례 없이 크고 대담한 문제를 다룰 수 있다는 관점임.

프로그래밍 언어 탐험의 새로운 개척지

  • LLM은 연구의 반사실적 질문을 전례 없는 속도로 답하고 시험하며 검증할 수 있는 매우 똑똑한 도구라는 평가임.
  • 최근 몇 달 동안 매일 새로운 아이디어가 떠올랐으며, 소프트웨어 생태계가 전제로 삼아 온 가정 가운데 상당수가 더는 성립하지 않는다는 관찰임. 가정을 하나씩 질문하는 과정에서 새롭고 흥미로운 연구 아이디어가 생김.
  • 인터프리터를 출시하라는 제안임. LLM은 지루한 증명을 처리하는 데 매우 뛰어나며, 인간이라면 수행하지 않았을 규모로 작업할 수 있음.
  • LLM에 문제를 제시하면 프로그램을 바이너리 수준까지 검증할 수 있다는 설명임. 이 능력을 이용해 해석형 언어의 의미론을 자동 생성하고, 생성한 의미론이 해당 언어의 구체적인 바이너리 동작을 추상화한다는 점을 증명하는 실험을 진행함.
  • 이 아이디어는 1년 전만 해도 상상하기 어려웠지만, 현재는 프롬프트 작업 한 달이면 가능하다는 평가임.
  • 인공지능 우선 검증 도구(진행 중)임. 검증 및 언어 도구는 인간 사용자의 한계를 중심으로 설계돼 왔음.
  • LLM의 강점과 약점은 인간과 비슷하면서도 완전히 같지는 않을 수 있으므로, 도구 내부의 세부 정보를 더 많이 드러내는 등 에이전트의 불균일한 지능에 맞춰 인터페이스를 조정할 가능성이 있음. 예시로 만족 가능성 모듈로 이론(SMT) 풀이기의 인스턴스화 그래프 공개가 제시됨.
  • 이러한 세부 정보를 노출해 LLM의 검증 도구 사용 능력을 높이는 실험을 Amazon과 진행 중임.
  • 새 언어의 의미론 개발(진행 중)임. 직장 동료들이 동역학계를 위한 새 언어 dynestyx를 개발했으며, 프로그래밍 언어 연구자는 아니지만 해당 분야의 많은 작업을 통합한 언어를 만드는 데 협력함.
  • 이 언어에는 형식 의미론이 없으며, 이를 구축하는 일은 충분히 도울 수 있는 전문 영역임. 그러나 해당 분야의 전문가가 아니고, 그 분야를 천천히 익힐 시간도 부족한 상황임.
  • 이에 새로운 협업 방식으로 LLM을 사용해 언어의 기계화된 큰 단계 의미론을 자동 생성하고, 테스트로 검증한 다음, 동료들과 함께 의도에 맞도록 의미론을 반복 조정하는 실험을 진행 중임.
  • 응용 분야뿐 아니라 이론 연구에서도 LLM의 잠재력이 큼. 증명 작성 작업을 자동화하면 반사실적 질문을 쉽게 던질 수 있음.
  • 언어에 특정 구문을 추가하면 여전히 강한 정규화 성질을 유지하는지 질문할 수 있음.
  • 타입 시스템을 바꾸면 여전히 건전한지 검토할 수 있음.
  • 이러한 질문을 이전에는 불가능했던 속도로 반복해서 탐구할 수 있음.
  • 놀라운 작업을 하는 데 필요한 수고가 줄어든 데서 어느 정도 상실감을 느낌. 과거에는 프로그래밍과 개발을 깊이 자랑스러워했으며, 낯설고 틈새적인 언어로 수십만 줄 규모의 프로젝트를 혼자 만들고 난해한 타입 시스템의 속성을 설계하고 증명하는 데 오랜 시간을 들였음.
  • 코드는 정성을 들이는 기술이었고 깊은 자부심의 원천이었지만, 이는 지적 호기심보다 자아에 가까웠다는 성찰임. 아이디어와 통찰, 탐험에는 반드시 자신의 전문성이 필요한 것은 아님.

새내기 프로그래밍 언어 연구자에게 작별과 즐거운 해킹을

  • 자아를 내려놓고 탐험의 즐거움에 자신을 맡기라는 권고임.
  • 연구는 언제나 탐험이자 인간 지식의 경계를 넓히는 일이었으며, 이것이 과학의 아름다움이자 과학자의 의미라는 관점임.
  • 더 많은 질문을 던지고 조사하며 깊이 파고들어야 함. 새로운 도구는 이전과 비교할 수 없는 방식으로 현실의 깊이를 질문하고 탐색하고 파헤칠 수 있게 하므로 이를 활용하고 즐기라는 제안임.
  • 프로그래밍 언어 탐험의 시대가 시작되며, 분야가 진정으로 변혁적인 순간에 들어서고 앞으로 펼쳐질 거칠고 기상천외한 미래가 기대된다는 전망임.