가브리엘라 모레이라, Informal Systems의 Quint CEO – 인터뷰 시리즈

가브리엘라 모레이라, Informal Systems의 Quint CEO는 프로그래밍 언어와 형식적 방법에 전문적인 연구 엔지니어로, 복잡한 시스템 검증을 엔지니어에게 더 쉽게 만드는 도구를 구축하는 데 강한 초점을 가지고 있습니다. 그녀는 TLA+를 기반으로 하는 현대적인 실행 가능한 사양 언어인 Quint의 개발을 주도하며, 언어와 그 도구를 계속 유지하고 발전시키고 있습니다. 그녀의 작업은 형식적 검증, 정적 분석 및 개발자 도구를 포함하며, 그녀는 또한 형식적 방법을 가르침으로써 학계에 기여했습니다. 이는 실제 엔지니어링과 이론적 깊이의 결합을 반영합니다.

Quint는 Informal Systems에서 개발 및 유지 관리되는 현대적인 사양 언어로, 분산 네트워크, 블록체인 및 데이터베이스와 같은 복잡한 시스템을 모델링, 테스트 및 검증하기 위해 설계되었습니다. Quint는 TLA+(Temporal Logic of Actions)의 기초 위에 구축되었으며, 더 개발자 친화적인 구문을 도입했으며, 유형 검사, 시뮬레이션 및 모델 검사와 같은 고급 도구를 제공하여 엔지니어가 배포 전에 시스템 오류를 감지할 수 있습니다. 이 플랫폼은 실행 가능한 사양을 강조하여 개발자가 시스템 동작을 설명하는 것 외에도 활발히 테스트하고 탐색할 수 있도록 합니다. 이는 이론적 정당성과 실제 구현 사이의 간격을 메웁니다.

처음으로 프로그래밍에 관심을 가지게 된 계기가 무엇이었으며, 어떻게 형식적 방법과 분산 시스템으로 관심을 가지게 되었나요?

나는 열렬한 게이머였으며, 나쁜 컴퓨터를 가지고 있었습니다. 그리고 문제를 해결하고 작동하게 만드는 것을 즐겼습니다. 컴퓨터 과학을 공부하기로 결정했고, 이론과 컴파일러에 끌렸습니다.

2015년에 프로그래밍 대회에 참여했습니다. 그 대회에서 예제 입력과 예상 출력을 제공받고, 문제를 해결하는 코드를 작성했습니다. 하지만 제출 후에 코드가 실제로 많은 예제로 테스트되는 것을 알게 되었습니다. 내가 생각하지 못한 경우에 코드가 실패할 수 있다는 깨달음이 프로그래밍을 도전으로 만드는 계기가 되었습니다.

업계에서 일하면서 분산 시스템에 관심을 가지게 되었습니다. 우리는 다양한 순서로 메시지가 도착할 수 있고, 다양한 실패 모드와 숨겨진 동작을 고려해야 했습니다. 2018년에 동료가 TLA+라는 형식적 사양 언어를 소개해 주었습니다. 나는 즉시 그것에 매료되었습니다. 나는 즉시 TLA+를 기반으로 하는 도구를 구축하기 시작했고, 그 분야에서 계속 작업해 왔습니다.

형식적 방법과 프로그래밍 언어를 중심으로 경력을 구축했습니다. Quint의 개발을 Informal Systems에서 주도하는 데 무엇이 동기를 부여했으며, 어떻게 형식적 검증을 더 쉽게 만들었습니다?

TLA+는 너무优秀하여 산업에서 광범위하게 사용되지 않도록 할 수 없습니다. 나는まだ khá 젊은 나이에 그것을 배웠고, 동료들과 함께 해결책을 찾기 위해 전화 회의에 참여했습니다. 하지만 나는 항상 마지막 방어선에 서있었습니다. 나는 더 나은 방법이 있을 것이라고 생각했습니다. 형식적 방법을 사용하여 사양을 만들고, 코드를 구현하기 전에 그것을 검증하는 것이 더 좋을 것이라고 생각했습니다. 그래서 나는 학문적 여정을 시작했습니다. 그것은 Informal Systems와 Quint로 이어졌습니다.

Quint는 처음에 제품으로 설계되지 않았습니다. Informal Systems에서 필요에 의해 구축되었습니다. 우리는 신뢰할 수 있는 시스템에 대한 TLA+ 사양을 작성했지만, 구문이 너무 어려웠고, 도구가 사람들의 기대에 못 미쳤습니다. 우리는 동료와 외부 협력자에게 보여주었습니다. “이것을 보세요, 나는 이것을 만들었습니다”라고 말했습니다. 하지만 그들은 읽을 수 없었고, 새로운 도구를 배우기에 시간이 없었습니다.

Quint의 설계 선택은 바로 그 경험에서 비롯되었습니다. 언어는 읽기 쉽고 기억하기 쉽습니다. 우리는 먼저 VSCode 확장 프로그램을 구축했습니다. 그것은 입력 중에 오류를 강조 표시했습니다. 유형과 효과 시스템이 있으며, 명시적으로 계층을 분리합니다. REPL이 있으며, 상호 작용적으로 탐색할 수 있습니다. 시뮬레이터가 있으며, 빠른 피드백을 받을 수 있습니다. JSON 형식의 추적을 내보내며, 기계가 구문 분석하기 쉽습니다. 이것들은 프로그래머가 이미 기대하는 도구입니다. 그리고 우리는 그것을 필요로 했습니다. 검증은 TLA+와 동일합니다.

Quint는 분산 시스템을 모델링하고 테스트하는 능력으로 강점을 가지고 있습니다. 이것은 블록체인이나 실시간 인프라와 같은 시스템을 구축하는 방법에 대한 엔지니어의 생각을 어떻게 바꿔야 합니까?

가장 큰 변화는 검증을 앞으로 이동하는 것입니다. Leslie Lamport, TLA+의 창시자는 사양을 코드 작성 전에 작성하는 것을 건축蓝图를 작성하는 것과 비교합니다. 이미 무엇인가를 구축했더라도, 지금 사양을 작성하고, 그것을 사용하여 추가적인 변경 사항을 알리는 것이 좋습니다.

소프트웨어 산업에서 우리는 마크다운 파일과 화이트보드를 사용합니다. 그것은 건물을 설명하는 것과 비슷합니다. 하지만 벽의 크기가 합계가 맞는지 알 수 있나요? Quint는 시스템을 설명할 수 있는 방법을 제공합니다. 높은 수준에서 설명할 수 있으며, 동작과 정당성에 대한 통찰력을 얻을 수 있습니다.

TLA+의 기초 위에 Quint를 구축했습니다. 어떻게 형식적嚴格性를 유지하면서 언어를 더 개발자 친화적으로 만들었나요?

중요한 결정은 Quint를 TLA의 일부로 제한하는 것이었습니다. TLA는 매우 표현력이 풍부하지만, 일부 표현력이 도구에서 지원되지 않으며, 사람們이 잘못 사용하여 디버깅이 매우 어려워집니다. 우리는 현실적인 사양에서 실제로 필요한 것에 집중하기로 결정했습니다. 혼란의 가능성을 피했습니다.

타입 시스템과 효과 시스템은 제약을 추가하지만, 유용한 제약입니다. 그것은 사양 오류를 방지합니다. 타입은 거의 모두 추론되며, 효과는 사용자에게 숨겨져 있습니다. 그래서 가치를 추가하지만, 마찰은 없습니다.

형식적 방법을 강의로 가르치면서, 엔지니어들이 형식적 검증에 대해 가지고 있는 가장 일반적인 오해는 무엇이라고 생각합니까?

나는 형식적 방법이나 형식적 검증에 대해 들어본 적이 없는 학부 학생들을 가르쳤습니다. 그래서 오해는 없었습니다! 교육 과정은 대부분의 학생들이 분산 시스템이나 스레드에 대해 배울 수 있도록 설계되었습니다. 나는 비를 경험하기 전에 우산이 무엇인지 가르치는 것과 비슷하다고 생각했습니다!

나는 형식적 방법과 공식적으로 시스템을 지정하는 방법이 해결책과 에지 케이스를 찾는 데 어떻게 도움이 될 수 있는지 가르치고 싶었습니다. 형식적으로 모든 소프트웨어를 검증해야 한다고 생각하도록 만들기보다는, 형식적 방법이 실제 상황에서 어떻게 도움이 될 수 있는지 보여주고 싶었습니다. 내 최종 과제는 테이블탑 RPG 설정이었습니다. 플레이어가 취할 수 있는 순서와 설정이 고려되어야 했습니다. 분산 시스템의 어려움을模擬하려고 했습니다. 그것은 학생들이 도구를 사용하여 에지 케이스를 찾고, 몬스터를 이기기 위한 해결책을 개선하도록 만들었습니다.希望적으로, 그들이 일에서 비슷한 상황을 직면할 때, 그들은 나를 기억할 것입니다. 일부 학생은 이미 기억하고 있습니다.

소프트웨어 개발에서 AI를 결합하는 관심이 증가하고 있습니다. Quint와 같은 도구를 사용하여 개발자가 공식적인 사양을 작성, 검증 또는 생성하는 데 AI가 도움이 될 수 있다고 생각합니까?

중요한 역할을 할 것입니다. 이미 일어나는 것입니다. 컴퓨터 과학은 코드 작성보다 더 넓은 분야입니다. AI는 형식적 방법을 사용하는 새로운 방법을 열어줍니다. LLM은 자연어 설명에서 Quint 사양을 작성할 수 있으며, 기존 코드에서도 작성할 수 있습니다. Quint LLM 키트에는 Claude Code 에이전트가 있으며, 프로토콜의 영어 설명에서 Quint 사양을 생성할 수 있습니다.

동시에 Quint는 AI로 작성된 코드를 신뢰할 수 있도록 도와줍니다. 나는 이해에서 오는 확신이 필요하다고 믿습니다. 코드 작성과 검증을 주도하는 Quint 사양을 작업하는 것은 개발자가 시스템의 동작을 이해하고, AI 생성 코드의 행동을 더 확신할 수 있도록 합니다. 이것은 AI 사용이 생성할 수 있는 인지 부채를 해결하고, 생성된 코드를 검증하는 더 확신할 수 있는 방법을 제공합니다.

형식적 방법이 소프트웨어 개발 라이프사이클의 표준 부분으로 이동하기 위해 무엇이 필요합니까?

일단, Quint에는 두 가지 중요한 것이 필요합니다. 비용을 낮추고, 가치를 높여야 합니다. 나는 이것이 다른 많은 것에도 적용된다고 생각합니다. 형식적 방법은 AI로 인해 큰 도약을 했습니다. 공식적인 사양을 작성하는 비용을 크게 낮추었으며, 이해와 신뢰가 부족한 환경에서 형식적 방법이 가장 영향력 있고 가치 있는 곳에서 그 가치를 높였습니다.

AI가 우리 직업을 바꾸고 있습니다. 적어도 어느 정도는 그렇습니다. 나는 이 변화가 더 높은 수준의 설계 선택과 행동의 정당성으로, 형식적 방법이 일상적인 도구가 되도록 바뀌기를 바랍니다. 개발자가 더 이상 코드나 시스템을 이해하지 못하고, AI 생성 코드를 검토하는 데 모든 시간을 보내지 않도록 바뀌기를 바랍니다.

감사합니다. 이 실행 가능한 사양 언어에 대해 더 알고 싶은 독자는 Quint를 살펴볼 수 있습니다.