아이디어와 인사이트

AI 퍼스트 개발, 코딩 가드레일, 그리고 폐기 가능한 아키텍처를 탐구합니다.

텍스트 에디터는 잘못된 코드를 쓰게 한다. 트리 에디터는 그렇지 않을 것이다.

모든 컴파일러는 코드를 트리로 보지만, 에디터는 원시 텍스트를 편집하게 한다. 구조화 편집이 실제로 어떤 모습인지, 왜 보편화되지 않았는지, 그리고 도구를 바꾸지 않고 그 이점을 얻는 방법을 설명한다.

모든 프로그래밍 언어에는 공식 문법이 있다. 컴파일러는 이를 읽고 parse tree를 구축하며, 맞지 않는 것은 모두 거부한다. 에디터는 문법을 완전히 무시하고 사용자가 원하는 대로 입력할 수 있게 한다. 이 괴리는 놀랄 만큼 많은 마찰의 원인이다. Autocomplete는 문맥상…

Donald Knuth는 프로그램을 문학처럼 읽히길 원했다. 컴파일러는 다른 생각이 있었다.

Literate programming은 코드를 먼저 인간을 위해, 그 다음 기계를 위해 작성해야 한다고 약속했다. 40년이 지난 지금, 거의 아무도 그렇게 쓰지 않는다. 소프트웨어 문서화에서 가장 우아한 아이디어가 우리의 작업 방식을 바꾸지 못한 이유는 다음과 같다.

1984년, Donald Knuth는 급진적인 전환을 제안하는 논문을 발표했다. 프로그램은 컴파일러를 위해 작성되고 인간을 위해 주석을 다는 것이 아니라, 인간을 위한 문학으로 작성되어야 하며, 컴파일러는 그로부터 실행 가능한 부분을 추출해야 한다. 그는 이를 literate…

버그를 고치는 건 쉬운 부분이다. 왜 그것이 존재하는지 파악하는 것이 중요하다

대부분의 팀은 결함을 고치고 넘어간다. 같은 결함이 다시 돌아온다. Fagan inspection 안에서 인과 분석을 실행하여 같은 버그를 두 번 쓰지 않는 방법을 알아본다.

모든 팀에는 계속 돌아오는 결함이 하나씩 있다. 페이지네이션의 오프바이원. 인증 미들웨어의 누락된 null 체크. 세 스프린트 전에 누군가 "고쳤다"는 체크아웃의 race condition. 같은 버그를 세 번 쓴 것이 아니다. 같은 원인을 가진 세 가지 다른 버그를 쓴 것이다.…

풀 리퀘스트 리뷰는 결함의 15~30%를 발견한다. 데이터는 50년 전부터 그랬다.

IBM, AT&T, HP, Microsoft를 대상으로 한 다수의 연구에서 비공식 코드 리뷰가 결함의 약 4분의 1을 발견함을 확인했다. 데이터가 실제로 말하는 바, 그 수치가 낮은 이유, 그리고 해결 방법을 소개한다.

비공식 코드 리뷰는 검토 대상 코드에 존재하는 결함의 15~30%를 발견한다. 이는 의견이 아니다. 40년이 넘는 기간, 여러 기업, 수십 개의 연구를 통해 재현된 결과다. 마이클 페이건은 1976년 IBM에서 이를 기록했다. 1987년 AT&T 벨 연구소의 연구에서는 20%를…

일반적인 체크리스트는 아무것도 찾지 못한다. 구조화된 체크리스트는 결함의 60%를 찾아낸다.

대부분의 리뷰 체크리스트는 단순히 복사-붙여넣기한 선의의 목록이다. Fagan inspection 스타일의 구조화된 체크리스트는 실제 결함 데이터를 기반으로 구축되며, 특정 아티팩트 유형을 대상으로 하고 개별 준비 과정에서 사용된다. 작동하는 체크리스트를 만드는 방법은 다음과 같다.

팀에 코드 리뷰 체크리스트가 있다면, 아묘도 열지 않는 위키 페이지에 묻혀 있을 가능성이 높다. 아마도 "check for off-by-one errors"나 "verify error handling" 같은 내용이 적혀 있을 것이다. 이것들은 사실이다. 하지만 행동을 바꾸기에는 너무…

대형 언어 모델은 코드를 미리 검토할 수 있다. 회의를 주관할 수는 없다.

파견 검사는 250줄을 검토하는 데 4~6명과 2시간이 필요하다. 대형 언어 모델은 준비 작업과 체크리스트 준수를 담당하여 비용을 줄일 수 있지만, 가장 비싼 결함을 찾아내는 인간의 역할을 대체할 수는 없다.

완전한 파견 검사에는 진행자, 낭독자, 2~4명의 검토자, 그리고 작성자가 필요하다. 팀은 한 시간에 125줄의 속도로 대략 250줄의 코드를 2시간 동안 검토한다. 작은 변경에도 8~12인시가 드는 셈이다. 대형 언어 모델은 250줄을 1초도 채 걸리지 않아 읽을 수 있다.…

Fagan Inspections는 테스트 전 90%의 결함을 찾아냈다. 그리고 우리는 그것을 멈췄다.

IBM의 Michael Fagan이 개발한 구조화된 검토 프로세스는 코드가 컴파일러에 도달하기 전에 거의 모든 결함을 포착했다. 동시에 총 프로젝트 노력의 15~20%를 소비했다. 소프트웨어 역사상 가장 효과적인 리뷰 방법이 사라진 이유와 팀이 실제로 놓친 것은 무엇인지 알아본다.

1976년 Michael Fagan은 IBM Systems Journal에 한 편의 논문을 발표했다. 거기에 기술된 리뷰 프로세스는 소프트웨어 품질의 금기준(gold standard)이 될 정도로 효과적이었다. Fagan Inspections는 단 하나의 테스트도 실행되기 전에 전체…

당신의 최고 리뷰어도 대부분의 결함을 놓친다. Fagan은 1976년 IBM에서 이를 측정했다.

시니어 엔지니어도 비구조화된 리뷰에서 결함의 극히 일부만 포착한다. Michael Fagan의 IBM 연구는 그 이유를 밝혔고, 이를 수정하기 위한 구조화된 인스펙션 프로세스를 구축했다.

두 명의 시니어 엔지니어가 동일한 풀 리퀘스트를 리뷰한다. 한 명은 누락된 null 체크를 지적한다. 다른 한 명은 클린업 패스의 레이스 컨디션을 발견한다. 둘 다 둘을 모두 찾지는 못한다. 리뷰어를 한 명만 배정했다면, 그 버그 중 하나는 출시되었을 것이다. 이것은 기술 격차가…

대부분의 코드 리뷰는 결함의 20%만 찾아낸다. Fagan Inspection은 90%를 찾아낸다.

비공식 코드 리뷰는 결함의 15~30%를 찾아낸다. 50년 된 구조화된 프로세스인 Fagan Inspection은 일관되게 60~90%의 제거율을 보고한다. 이것이 어떻게 작동하는지, 팀이 이를 피하는 이유, 그리고 경량 버전을 실행하는 방법을 알아본다.

대부분의 코드 리뷰는 원래 찾아야 할 결함의 15~30%를 포착한다. 이는 추측이 아니다. IBM은 1970년대에 이를 측정했고, AT&T, HP, Microsoft의 연구가 수십 년에 걸쳐 동일한 범위를 확인했다. 비공식 리뷰는 저렴하고, 비동기적이며, 사회적으로 받아들여진다.…

AutoVerus는 40시간의 증명 작성을 3회의 LLM 호출로 만든다. 비결은 포기할 때를 아는 것이다.

AutoVerus는 LLM 에이전트 네트워크를 사용해 Rust 코드에 대한 Verus 정합성 증명을 생성하며, SMT 솔버 피드백에 의해 구동되는 생성-수정-디스차지 루프를 통해 90% 이상의 증명 의무를 자동화한다.

형식 검증에서 가장 어려운 부분은 검증기 자체가 아니다. 증명을 작성하는 것이다. 숙련된 Rust 엔지니어에게 Microsoft Research의 SMT 기반 검증기인 Verus를 주면, 오후 한때에 함수에 precondition과 postcondition을 주석으로 달 수 있다.…