AI 퍼스트 개발, 코딩 가드레일, 그리고 폐기 가능한 아키텍처를 탐구합니다.
클린룸 검증은 검증 조건을 생성하고 해소하는 것을 요구한다. 여기서 LLM이 주석과 VC 생성을 자동화하여 실제 어려운 증명에 집중할 수 있게 하는 방법을 소개한다.
클린룸 소프트웨어 공학은 코드를 컴파일하기 전에 그 정당성을 증명할 것을 요구한다. 그것은 고귀하게 들리지만, 열 개의 정수를 정렬하는 함수를 위해 루프 불변식을 세 시간 동안 작성하다 본다면 상황이 달라진다. 병목 지점은 증명 자체가 아니다. 상용구이다. 검증 조건을 생성하고,…
Cleanroom software engineering 은 defect rate 를 100배 낮추지만, 완전 도입에는 별도의 test team 과 formal proof 가 필요하다. 여기서는 overhead 없이 그 대부분의 benefit 을 얻을 수 있는 pragmatic subset 을 소개한다.
Cleanroom software engineering 은 1,000줄당 0.1개의 defect 를 달성한다. 업계 평균은 10에서 50이다. 문제는 완전한 Cleanroom 을 위해서는 팀을 author 와 verifier 로 분할하고, 모든 module 앞에 formal…
IBM의 Cleanroom engineering은 업계 평균보다 100배 나은 defect rate를 달성한 뒤 사라졌다. 사라진 이유는 그것이 작동했는지와는 아무런 관련이 없었다.
IBM의 Cleanroom software engineering process는 천 줄당 0.1개의 defect를 달성했다. 당시 업계 평균은 10에서 50 사이였다. 이 process는 문서화되었고, 여러 프로젝트와 언어에 걸쳐 replicate되었으며, 독립적으로 검증되었다.…
Cleanroom software engineering은 디버깅 대신 mathematical verification을 통해 zero-defect increment를 약속했다. 우리는 IBM의 실제 프로젝트 데이터를 살펴보아 그 주장이 성립했는지 본다.
1980년대 소프트웨어 업계 평균은 천 줄당 30~60개의 결함이었다. IBM의 Cleanroom 팀은 2만 줄짜리 컴파일러 인크리먼트를 테스트에서 53개의 결함이 발견된 상태로 출시했다. 이는 KLOC당 2.6개이다. 1만 줄짜리 개별 인크리먼트 중 일부는 시스템 테스트에서 결함이…
Box Structure는 모듈이 무엇을 하는지, 무엇을 기억하는지, 어떻게 동작하는지를 세 개의 별개이면서 검증 가능한 겹으로 정의하도록 강제한다. Cleanroom이 어떻게 디버깅을 제거하는지 알아보자.
먼저 코드를 쓰고, 다음에 테스트를 쓰고, 그제야 코드가 틀렸다는 걸 알게 된다. 이게 표준 루프다. 그래서 디버깅은 대부분의 프로젝트 타임라인 절반을 잡아먹는다. Box Structure는 이를 뒤집는다. 코드를 쓰기 전에 동작을 정의하고, 그 정의를 수학적으로 검증한 뒤, 한 겹씩…
IBM의 Cleanroom 엔지니어링 프로세스는 버그를 찾는 대신 미연에 방지함으로써 업계 평균보다 100배 우수한 결함률을 달성했다. 이것이 어떻게 작동했는지, 왜 거의 아무도 사용하지 않는지, 그리고 오늘 당신이 도입할 수 있는 것은 무엇인지 알아보자.
IBM은 NASA 위성 제어 시스템을 천 줄당 0.1개 결함이라는 수준으로 출시했다. 당시 업계 평균은 10에서 50 사이였다. 그들이 이를 달성한 것은 더 똑똑한 엔지니어를 고용하거나 더 오래 일해서가 아니다. 개발자가 자신의 코드를 실행하지 못하게 함으로써 달성한 것이다. 이것이…
Literate programming은 단일 진실 공급원을 약속하지만, 수동 weave와 tangle 단계가 CI/CD 파이프라인을 망친다. Markdown 파일이 정규 소스로 남도록 추출과 문서 생성을 자동화하는 방법을 소개한다.
빌드 파이프라인이 터미널을 열고 을 입력하지 않으면 실행될 수 없다면, 당신은 리터레이트 프로그램을 가지고 있지 않다. 컴파일러가 달린 일기장을 가지고 있는 것이다. 리터레이트 프로그래밍의 전체 목적은 산문과 코드가 단일 진실 공급원을 공유하는 것이다. Markdown 파일이…
30일 동안 LLM에 코드를 요청하기 전에 설계 설명을 작성했다. 그 결과는 내가 rubber-ducking을 바라보는 방식을 바꿔 놓았다.
대부분의 개발자는 LLM을 거꾸로 사용한다. 다섯 단어로 원하는 것을 설명하고, 200줄의 코드를 받은 뒤, 다음 한 시간은 모델이 내린 가정을 디버깅하는 데 쓴다. 나는 반대 workflow를 3개월간 실행했다. 한 줄의 코드도 요청하기 전에 완전한 설계 설명을 작성하는 것이다.…
Literate programming은 Markdown 파일을 single source of truth로 삼아 문서, 테스트, 구현체를 동기화 상태로 유지한다. Python 30줄로 구현하는 방법을 소개한다.
당신의 문서, 테스트, 코드는 동일한 이야기를 제대로 전달하지 못하는 세 개의 파일이다. 소스의 함수 시그니처를 업데이트한다. README 예제를 잊는다. 일주일 후, 신입 사원이 오래된 스니펫을 프로덕션에 복사한다. 테스트 파일은 여전히 예전 동작을 예상 결과로 인코딩하고 있다.…
LLM 대화에는 의도, 거부된 대안, 그리고 작동하는 코드가 담겨 있습니다. 이것이 바로 문서가 되어야 할 것입니다. 다음은 일회성 채팅을 내러티브를 잃지 않고 지속 가능하고 검색 가능한 문서로 전환하는 방법입니다.
당신은 Claude와 45분을 들여 재시도 회로를 설계했다. 실패 모드를 설명하고, 계단식 압력을 숨기기 때문에 지수 백오프를 거부한 뒤, jitter가 포함된 token-bucket rate limiting으로 결정하고 작동하는 구현을 생성했다. 설명은 명확했고, 추론은 타당했으며,…