코드를 더 빠르고 정확하게 작성하기 위해 단조성, 사전·사후 조건, 불변식, 격리, 귀납법을 머릿속의 작은 증명으로 활용하는 방법을 설명합니다.
코드를 더 빠르고 정확하게 작성하는 데 도움이 되는, 내가 배운 한 가지 요령을 간략히 소개하려 한다. 나는 이를 “요령”이라고 부르지만, 사실 경력이 쌓여 가면서 알아차리지 못한 채 시작하게 된 일에 가깝다.
어려운 작업을 할 때는, 코드를 작성해 나가며 그 코드가 실제로 원하는 일을 할 것이라는 증명을 머릿속에 그려 보라. 단순한 생각이지만 말처럼 쉽지는 않다. 흐름을 끊지 않고 이를 “온라인으로” 해내려면 많은 연습이 필요하다. 하지만 정말 능숙해지면, 놀랄 만큼 자주 코드가 첫 번째나 두 번째 시도에 작동한다는 것을 알게 될 것이다. 약간 마법처럼 느껴진다.
이를 해내는 방법은 많고, 지나치게 규정하고 싶지는 않다. 그저 내가 즉석에서 추론하곤 하는 종류의 몇 가지 예를 나열해 보겠다. 그러면 전반적인 감을 잡을 수 있을 것이다.
코드에 관해 스스로 무언가를 증명할 때 주의 깊게 살펴볼 대상 중 하나는 어떤 부분이 _단조적_인가 하는 점이다.
수학의 단조 함수는 아마 익숙할 것이다. 비공식적으로 말하면, 이는 “뒤로 가지 않는” 함수다. 즉 증가 단조 함수는 증가하거나 그대로일 수만 있고, 감소 단조 함수는 감소하거나 그대로일 수만 있다. 각각 비감소 함수와 비증가 함수라고도 한다.
단조 _코드_라는 개념은 단조 함수라는 개념보다 조금 더 모호하지만, 한 방향으로만 진행할 수 있는 과정이라는 같은 생각을 담고 있다. 예를 들어 체크포인팅은 단조성의 훌륭한 사례다. 여러 작업을 순서대로 수행해야 하는 스크립트가 있다고 하자. 지금까지 완료한 작업 수를 나타내는 상태 정보를 디스크에 보관할 수 있다. 무언가 잘못되어 스크립트가 충돌하면, 디스크의 상태를 확인해 어디까지 진행했는지 파악한 뒤 아직 실행되지 않은 가장 이른 상태부터 다시 시작할 수 있다.
체크포인팅은 스크립트의 “현재 단계” 포인터가 앞으로만 갈 수 있음을 뜻한다. 스크립트는 이미 수행한 단계를 되돌아가 다시 실행할 수 없기 때문이다. 이런 의미에서 스크립트는 단조적으로 진행하며, 스크립트가 성공적으로 완료된다면 모든 단계를 정확히 한 번씩 실행했음이 분명하다.
이런 종류의 활동 로그를 유지하는 것은 단순한 생각이지만 저널링 파일 시스템과 데이터베이스의 선행 기록 로그처럼 놀라운 곳에서 자주 등장한다. 좀 더 복잡한 데이터베이스 사례로는 LSM 트리가 있다. LSM 트리는 일부 데이터베이스에서 행을 메모리와 디스크에 저장하는 데 사용되며, 대부분의 경우 순수하게 추가만 이루어진다. 느슨하게 말하면, LSM 트리는 모든 삽입, 삭제, 갱신의 로그를 유지하고 행을 읽을 때 로그를 훑어 해당 행의 적절한 값을 재구성한다. 오래된 연산은 컴팩션이라는 과정에서 공간을 절약하기 위해 주기적으로 버려진다. LSM 트리가 차지하는 공간은 오직 증가한다. 단, 컴팩션 중에는 오직 감소한다.
이를 행을 제자리에서 삭제하고 갱신하는 더 전통적인 데이터베이스 구조인 B-트리와 비교할 수 있다. B-트리는 일반적으로 삭제 후 해제된 공간을 회수하고, 갱신으로 행이 커질 때 공간이 생기도록 구조를 재편하며, 버퍼가 충분한지 확인하는 등의 일을 훨씬 더 많이 해야 한다. 원한다면 B-트리와 LSM 트리에 관해 조금 더 읽어 보고, 어느 쪽이 추론하기에 더 직관적으로 느껴지는지 살펴보라.
단조성은 보통 가능한 결과의 넓은 범위를 배제하는 데 사용할 수 있으므로 주의 깊게 살펴볼 가치가 있다. 이 주제의 또 다른 변형은 불변성이다. 여러 면에서 단조성의 사촌 격인 개념인데, 불변 객체를 만들면 그 객체는 수정될 수 없다. 값은 객체를 생성할 때 정확히 한 번만 불변 객체에 할당할 수 있으며, 할당을 “되돌리거나” “취소할” 수 없다. 덕분에 객체가 모르는 사이에 바뀔 수 있는 모든 시나리오를 단번에 무시할 수 있다.
사전 조건과 사후 조건은 함수의 동작에 관한 제약을 명시하는 방법이다. 함수의 _사전 조건_은 함수가 실행되기 직전에 참이라고 가정되는 것들이다. 이는 함수 입력에 대한 조건일 수도 있고, 프로그램의 상태나 환경에 관한 더 일반적인 주장일 수도 있다. 함수의 _사후 조건_은 함수가 반환된 직후 참이라고 가정되는 것들이다. 사전 조건과 마찬가지로, 이 주장들은 거의 무엇이든 포함할 수 있다. 함수가 실행되기 전에 사전 조건이 참이고 함수가 끝난 뒤 사후 조건이 참이 아니라면, 적어도 명시된 제약에 따르면 그 함수는 올바르게 구현되지 않은 것이다.
이는 단순한, 심지어 자명한 개념이며 그 자체로 증명 기법은 아니다. 하지만 형식적인 관점에서 이들이 무엇인지 계속 추적하는 것만으로도 추론에 도움이 될 수 있다.
(때로는 함수에 잘 정의된 사전 조건과 사후 조건이 없다는 사실을 발견할 수도 있는데, 이 역시 알아두면 좋다!)
특히 사후 조건을 명확히 정하는 것은 단위 테스트 아이디어를 만들어 내는 좋은 방법이다. 사전 조건과 사후 조건이 참임을 방어적으로 단언하고, 그렇지 않으면 충돌하도록 만드는 것도 도움이 될 수 있다. 그러면 코드가 충돌하지 않는 경우 무엇을 할지 더 쉽게 추론할 수 있다. 기껏해야 중립적인 절충처럼 들릴 수 있지만, 예측할 수 없는 방식으로 동작하는 것보다 일찍 충돌하는 편이 대개 더 안전하다.
코드 조각의 _불변식_은 무슨 일이 있어도 그 코드가 실행되기 전, 실행 중, 실행 후에 항상 참이어야 하는 것들이다. 사전 조건과 사후 조건처럼, 불변식도 거의 무엇이든 포함할 수 있다.
일관성을 불변식의 관점에서 생각하면 유용할 수 있다. 이런 상황에서 불변식은 “이 데이터 구조는 일관되고 유효하다”이며, 무슨 일이 일어나든 코드가 모든 지점에서 그 불변식을 보존한다는 것을 스스로 증명해야 한다. 이를 쉽게 하는 방법은 코드를 원자적인 “단계”로 나누고, 각 단계가 그 자체로 불변식을 보존함을 증명하는 것이다. 그러면 어떤 단계가 실행되든, 또 어떤 순서로 실행되든 불변식이 유지된다고 결론지을 수 있다.
가장 오래되고 유명한 불변식 사례 중 하나는 복식부기의 토대인 회계 등식이다. 회계 등식은 느슨하게 말해 회사 원장의 차변 총액이 대변 총액과 같아야 한다고 말한다. 올바르게 수행된 복식부기가 이 불변식을 보존한다는 것은 쉽게 증명할 수 있다. 모든 거래에서 대변 계정의 모든 증가분 또는 감소분은 차변 계정의 모든 증가분 또는 감소분과 같아야 한다. 거래 전 차변과 대변이 균형을 이룬다면 거래 후에도 균형을 이룬다는 것을 쉽게 알 수 있다. 따라서 불변식은 항상 보존된다.
특정 종류의 불변식을 유지하는 또 다른 방법은 리스너나 생명 주기 메서드를 사용해 특정한 중요한 지점에서 불변식이 참으로 유지되도록 하는 것이다. 이 기법은 여러 상태 조각을 동기화해야 할 때 자주 쓰인다. 예를 들어 C++는 생성자와 소멸자를 사용하여 객체에 필요한 메모리가 객체가 실제로 존재하는 동안에만 할당된 상태로 남도록 보장한다. useEffect는 React 컴포넌트에 대해 비슷한 일을 한다.
(불변식은 가능한 모든 시나리오에서 유지되어야 하므로, 상대적으로 적은 새 실행 경로를 도입하는 변경을 할 때 보통 더 쉽게 추론할 수 있다.)
나는 오랫동안 소프트웨어의 “기술” 중 _상당 부분_이 기존 시스템을 불안정하게 만들지 않고 수정하거나 확장하는 데 중심을 두고 있거나, 그래야 한다고 확신해 왔다. 코드베이스를 수정할 때, 바꾸려 의도하지 않았던 동작이 실제로 바뀌지 않았음을 어떻게 증명할지 아는 것은 매우 유용할 수 있다.
이를 스스로 증명하기 위해 자주 의지하는 기법이 있다. 이것에 이름이 있는지는 모르겠고, 기법이라기보다 사고 패턴이라고 부르는 편이 맞을지도 모르겠다. 가장 잘 설명하자면 이렇다. 모든 변경에는 “영향 반경”이 있다. 코드 한 부분의 변경은 시스템 전체의 일관성이나 정확성을 보장하기 위해 다른 부분의 변경을 필요로 할 수 있다. 이 두 번째 변경은 세 번째 부분의 변경을 요구할 수 있고, 계속 이어질 수 있다. 변경이 어떤 동작에 영향을 주고 주지 않는지 확정하려면, 변경이 특정 지점을 넘어 전파되는 것을 막을 수 있는 구조적 “방화벽”을 식별해야 한다. 이는 캡슐화의 개념적 사촌과도 같다.
이 생각은 꽤 추상적이므로, Nerve의 예를 들어 보겠다.
Nerve는 사용자가 많은 데이터 소스를 하나의 거대한 API인 것처럼 질의할 수 있게 해 주는 쿼리 엔진이다. Nerve 쿼리 파이프라인은 쿼리 실행을 위한 구체적인 단계별 계획을 계산하는 _쿼리 플래너_와, 그 계획을 수행하는 _쿼리 실행기_로 구성된다. Nerve의 쿼리에는 물질화 필드와 가상 필드가 모두 포함될 수 있다. 가상 필드는 기본적으로 파생 필드다. 다시 말해 물질화 필드는 소스 API에서 직접 가져오는 반면, 가상 필드는 다른 가상 또는 물질화 필드로부터 실행 시간에 계산된다.
물질화 필드는 다루기 꽤 쉽다. 적절한 요청을 만들고 필요에 따라 응답에서 데이터를 가져오면 된다. 가상 필드는 조금 더 까다롭다. 가상 필드가 다른 필드에 의존하는 경우가 있기 때문이다. 가상 필드를 계산하기 전에 그 가상 필드의 모든 선행 조건을 갖추었는지 보장해야 한다. 사용자에게 이러한 선행 조건을 직접 쿼리에 추가하라고 요구하는 것은 불필요하게 번거롭다. 대신 가상 필드를 계산하기 전에 그 의존성을 가져오는 장치가 있어야 한다. 하지만 이 장치는 어디에 두어야 할까?
한 가지 간단한 선택지는 쿼리 플래너와 쿼리 실행기를 모두 수정해, 쿼리에 명시된 대상이 아니라 의존성으로 가져오는 물질화 필드라는 개념을 부여하는 것이다. 이러한 “의존성 필드”는 가상 필드 계산에 사용할 수 있도록 보관해야 하지만 최종 쿼리 결과에 포함되어서는 안 된다. 염두에 두어야 할 다른 설계 고려 사항도 있다. 예를 들어 “일반” 물질화 필드를 가져올 때 만드는 요청과 동일한 요청에서 이 의존성 필드를 가져올 방법을 찾고 싶을 것이다.
이는 기본적으로 쿼리 파이프라인의 확장이다. 다소 복잡할 수는 있지만, 분명히 가능하다. 다만 여기에는 문제를 과도하게-가져온 뒤 사후에 정리하여 피하는 요령이 있다.
두 번째 접근법에서는 새로운 개념을 전혀 도입하지 않는다. 대신 쿼리 계획 중에 각 가상 필드의 의존성을 계산하여 단순히 쿼리에 추가한 다음, 쿼리 실행기에 넘긴다. 쿼리 실행기는 자신이 받는 쿼리가 사용자가 작성한 쿼리가 아니라는 사실을 전혀 모른다. 그저 평소처럼 쿼리를 실행해 먼저 모든 물질화 필드를 가져오고, 그다음 관련 가상 필드를 계산한다. 그리고 어떻게든 필요한 의존성이 항상 마법처럼 존재하므로 가상 필드의 의존성을 가져올 필요가 전혀 없다!
쿼리 실행이 완료된 뒤에는 사용자가 요청한 것보다 엄격히 더 많은 필드를 포함하는 쿼리 결과를 얻게 된다. 그래서 마지막에 사용자의 쿼리에 없던 필드를 제거하는 가지치기 단계를 추가한다.
이 해결책의 가장 큰 장점은 변경이 쿼리 파이프라인의 시작과 끝에 있는 두 작은 계층에 완전히 한정된다는 것이다. 중간의 요소들, 즉 쿼리 엔진의 “핵심”은 전혀 바꿀 필요가 없다. 특히 쿼리 플래너와 쿼리 실행기 사이의 경계는 변경이 전파되는 것을 막는 “방화벽” 역할을 한다. 따라서 의존성을 가져올 필요가 없는 쿼리를 실행할 때 우리의 변경이 회귀를 일으키지 않는다는 것을 아주 쉽게 증명할 수 있다. 그런 경우에는 손대지 않은 코드만 실행하기 때문이다!
이런 접근법이 적절할 때도 있고 그렇지 않을 때도 있지만, 다른 조건이 같다면 가능한 한 많은 코드를 건드리지 않는 편이 인지 부하를 줄인다.
(개방-폐쇄 원칙의 맥락에서 이 아이디어를 들어 본 적이 있을지도 모른다. 이 원칙에는 여기와 관련 없는 여러 객체 지향 프로그래밍 세부 사항이 포함된다. 여기서 중요한 것은 그 뒤에 있는 철학, 즉 “요구 사항이 바뀔 때 [프로그램]의 동작은 이미 작동하는 오래된 코드를 변경하는 대신 새로운 코드를 추가해 확장하라”는 것이다.)
흥미로운 프로그램 다수는 재귀 함수나 재귀 데이터 구조를 포함한다. 또한 특정한 이론적 의미에서 재귀는 계산 행위 자체의 중심에 있다. 작업하는 분야에 따라 재귀를 끊임없이 접할 수도, 가끔만 접할 수도 있지만, 어느 경우든 이를 추론하는 법을 알면 삶이 훨씬 편해질 수 있다.
재귀 데이터 구조는 자기 자신의 사본을 포함하는 구조다. 반드시 정확한 사본일 필요는 없지만, 같은 “유형”의 구조 인스턴스다. 이 사본에는 또 사본이 들어 있을 수 있고 계속 이어진다. 이 과정은 영원히 계속되거나 “기저 사례”에서 끝난다. 예를 들어 프랙털은 재귀적이다.
컴퓨터 과학에서 재귀 데이터 구조의 고전적 사례는 트리다. 트리는 일정 수의 자식을 가진 노드이며, 각 자식도 그 자체로 트리다. 자식이 없는 트리는 리프라고 하며, 이것이 기저 사례다.
리스트도 재귀적으로 표현할 수 있지만, 보통 그런 방식으로 생각하지는 않을 수 있다. 모든 재귀 리스트는 리스트의 “첫” 또는 가장 왼쪽 요소인 _헤드_와, 리스트의 나머지 요소를 담는 _테일_로 이루어진다. 테일은 그 자체로 리스트이며, 기저 사례 리스트는 빈 리스트다. 비슷한 맥락에서 자연수도 재귀적이라고 생각할 수 있다. 모든 자연수는 더 작은 다른 자연수에 1을 더한 것이며, 기저 사례인 0은 예외다.
재귀 _함수_는 자기 자신을 호출하는 함수다. 재귀 함수는 보통 재귀 데이터 구조를 처리하는 데 쓰인다. 재귀 사본에 대해 자기 자신을 호출할 수 있기 때문이다. 예를 들어 트리를 처리하는 함수는 모든 자식 트리에 대해 자신을 호출할 수 있다.
재귀 구조를 다루기 위해 꼭 맞게 만들어진 증명 기법도 있는데, 이를 _귀납법_이라고 한다. 귀납법의 “고전적” 형태는 어떤 명제가 임의의 자연수에 대해 참임을 증명하는 데 사용된다. 이를 증명하는 단계는 두 가지다.
두 번째 단계는 _귀납 단계_라고 하며, 성립한다고 가정하는 내용은 _귀납 가설_이라고 한다. 귀납 단계에 귀납법의 진정한 힘이 있다. 귀납 가설을 사용할 수 있게 되면 증명하기가 훨씬 쉬운 경우가 많다. 귀납법의 요점은 모든 수에 대해 한꺼번에 증명하려는 대신, 증명의 “점진적” 버전을 작성하는 것이다.
재귀 함수를 작성할 때는 귀납법을 사용해 그 정확성을 스스로 증명해 보라. 다음은 Nerve 코드베이스를 느슨하게 각색한 간단한 사례다.
지나치게 세부 사항에 들어가지 않고 말하면, Nerve에는 사용자를 위해 AST를 시각화해야 하는 특정 사례가 있다. 전체 AST는 꽤 복잡하므로, 표시하기 전에 사용자가 아마 신경 쓰지 않을 노드를 제거해야 한다. 노드를 제거할 때 그 노드의 부모는 “그 모든 자식을 상속해야” 한다. 기술적으로 말하면, 제거된 노드와 그 부모 사이의 간선을 수축해야 한다.
용어에 관한 짧은 설명: 기술적으로 수축은 간선에만 적용되는 용어지만, 여기서는 약간 편의상 노드와 트리를 수축한다고도 말하겠다. “노드를 수축한다”는 말은 “노드와 그 부모 사이의 간선을 수축한다”는 뜻이다. “트리를 수축한다”는 말은 “트리의 어떤 간선을 수축한다”는 뜻이다.
다음은 Nerve에서 사용하는 함수다. 정확히 같은 함수는 아니지만, 요지는 전달한다.
function simplifyTree(root: Node): Node {
let newChildren = [] as Array<Node>;
for (const child of root.children) {
const simplifiedChild = simplifyGraph(child);
if (shouldContract(simplifiedChild)) {
for (const grandChild of simplifiedChild.children) {
newChildren.push(grandChild);
}
} else {
newChildren.push(simplifiedChild);
}
}
root.children = newChildren;
return root;
}
우리는 이 함수가 주어진 AST를 가능한 한 많이 단순화하기를 원한다. 다시 말해 사후 조건은 다음과 같다. simplifyGraph가 반환하는 그래프는 “완전히 수축된” 상태여야 한다. 즉 더 이상 수축할 수 있는 간선이 없어야 한다.
다음은 이 조건이 실제로 성립한다는 귀납적 증명이다.
기저 사례부터 시작하자. 정의상 루트 노드는 자신을 합쳐 넣을 부모가 없으므로 수축될 수 없다. 따라서 기저 사례인 단일 리프 노드는 이미 사후 조건을 만족한다. simplifyGraph에 리프 노드를 전달하면 그 노드를 있는 그대로 반환할 뿐이므로, 기저 사례에서는 올바르게 작동한다고 결론지을 수 있다.
이제 마법의 시간, 즉 귀납 단계다. 트리의 모든 부분 트리에 대해 simplifyGraph가 올바르다면, 트리에 대해서도 올바르다는 것을 증명해야 한다. 결정적으로 이제 귀납 가설을 사용할 수 있으므로, 각 부분 트리, 즉 simplifiedChild를 루트로 하는 각 트리는 더 이상 수축할 수 없다고 가정할 수 있다.
새롭게 고려해야 할 수축 가능성은 simplifiedChild와 root 사이뿐이다. simplifiedChild를 수축해야 한다고 판단하면, 이를 제거하고 그 모든 자식을 root에 접목한다. 각 simplifiedChild에 대해 이를 수행한 뒤에는 root를 루트로 하는 트리가 더 이상 수축될 수 없음을 확실히 안다. 만약 수축할 수 있다면 적어도 하나의 부분 트리가 수축될 수 있다는 뜻이고, 이는 귀납 가설과 모순되기 때문이다. 증명 끝!
이런 종류의 귀납적 추론을 본능적으로 하기 시작하면 재귀 함수를 다루기가 더 쉬워질 수 있다.
(원한다면 귀납법을 사용하지 않고 전체론적으로 추론하여 simplifyGraph가 가능한 모든 입력에 대해 올바르게 작동한다는 것을 스스로 납득해 보라. 어떤 접근법이 더 자연스럽게 느껴지는가?)
지금까지의 내 주장은 “코드에 관해 머릿속으로 작은 증명을 작성하려 해야 한다” 정도다. 하지만 이 글에는 사실 비밀스러운 쌍대 버전도 있다. 즉 “작은 증명을 작성하기 쉬운 형태로 코드를 작성하려 해야 한다”는 것이다.
마찬가지로 이 글의 각 절에도 저마다 쌍대 형태가 있다.
핵심은 코드에 관해 얼마나 쉽게 추론할 수 있는지로 코드의 품질을 판단할 수 있다는 것이다. 코드가 올바르다는 것을 스스로 쉽게 증명할 수 있다면, 아마 꽤 잘 설계된 코드일 것이다. 반대로 지속적으로 답답하거나 어렵다면, 더 직관적으로 만들기 위해 코드를 정리하거나 재구성하는 것을 고려해야 한다.
이 품질을 “증명 가능성”이라고 부르고 싶었지만, 그 용어는 이미 존재하고 다른 의미를 지니므로 대신 “증명 친화성”이라고 부르겠다.
위의 제안에서 보이듯, 최대의 증명 친화성을 위해 설계하는 것은 적어도 주관적으로는 가능하다.
물론 증명 친화성만이 중요한 소프트웨어 품질의 차원은 아니다. 코드가 올바르고 빠르며 가능한 한 사용하기 쉬워야 한다. 하지만 이는 매우 중요한 차원이라고 생각한다. 결국 코드를 구축하고, 확장하고, 개선하고, 테스트하려면 코드가 무엇을 하는지, 무엇을 하지 않는지, 무엇을 할 수 있는지 이해해야 하기 때문이다. 거창하게 들릴 수 있지만, 중요한 의미에서 증명 친화성은 좋은 프로그래밍의 촉매라고 생각한다!
처음에 언급했듯, 여기서 이야기한 유형의 미시적 추론은 거의 생각하지 않고 할 수 있게 된 뒤에야 효과를 내기 시작한다. 타자도 그런 면에서 비슷하다. 독수리 타자보다 터치 타자를 아는 것이 시간을 절약하는 것은 그것이 사실상 본능이 되었을 때뿐이다. 두 경우 모두 직관을 기르려면 연습이 필요하다! 지름길은 없다고 생각한다. 그냥 시간을 들여야 한다.
이를 하는 가장 좋은 방법은 더 많은 수학적 증명을 작성하는 것이라고 생각한다. 프로그램에 관한 증명을 작성하는 것은 분명 도움이 되겠지만, 어떤 주제이든 증명을 구성하는 단순한 행위 자체가 복잡한 시스템을 다룰 때 유용한 논리적 사고를 연마하는 훌륭한 방법이라고 생각한다. 단, 그 증명을 작성해야 하며 읽기만 해서는 안 된다. 연습문제를 풀어라! 나 자신의 경우 얼마 전부터 재미로 수학을 하기 시작했고, 증명을 작성하는 일이 다양한 상황에서 사고의 명료함을 높이는 데 도움이 되었다는 것을 알아차렸다.
어디서 시작해야 할지 모르겠다면, 나는 EdX에서 Stanford의 학부 알고리즘 수업을 듣고 있다. 훌륭한 교수의 재미있고 증명 중심적인 강의다!
또 다른 좋은 훈련 장소는, 말하기는 싫지만, Leetcode다. 많은 사람과 마찬가지로 나는 Leetcode _면접_에 심각한 단점이 있다고 생각한다. 하지만 많은 문제가 증명 작성 근육을 단련할 만큼 충분히 어렵기 때문에, 혼자 연습하는 데는 유용할 수 있다. 시간을 재지 않아도 된다. 나는 보통 재지 않는다. 또한 풀이에 “요령”이 있는 문제는 피하려고 해 보라. 대신 적어도 일부 난제가 모든 것을 올바르게 정식화하고 구현하는 데 있는 문제를 찾아라. 가능한 한 적은 시도만으로 성공적으로 제출하는 데 집중하라. 문법 오류 같은 사소한 문제가 생겨도 괜찮다.
즐거운 코딩과 증명을!