The next fifty years

• 번역
• 주석

• 원문
  • The next fifty years (PDF)
  • The next fifty years (html)

이 글은 데이크스트라가 1995년에서 2000년 사이에 작성한 문서 The next fifty years (PDF)를 번역한 것입니다. 의역이 많으므로 원문과 대조해가며 읽기를 권합니다.

번역

The next fifty years

앞으로의 50년에 대하여

When the idea to write about the next fifty years of computing first entered my head, I wrote it off as utterly preposterous: which sane scientist purports to be able to see so far into the future? But then I realized that in a way that is precisely what educators do all the time: when designing our courses, we do dare to decide what to teach and what to ignore, and we do this for the benefit of people, many of whom will still be active forty to fifty years from now. Clearly some vision of the next half century of computing science is operational. To this I should add that it is all right if the crystal ball is too foggy to show much detail. Thirty-five years ago, for instance, I had no inkling of how closely program design and proof design would come together, and in such a detailed sense my life had been full of surprises. At the same time these surprises were developments I had been waiting for, because I knew that programming had to be turned into an endeavour amenable to some sort of mathematical treatment, long before I knew what kind of mathematics that would turn out to be. In other words, when building sand castles on the beach, we can ignore the waves but should watch the tide.

컴퓨팅 분야의 앞으로의 50년에 대해 글을 써야겠다는 생각이 처음 떠올랐을 때, 나는 그것이 완전히 터무니없는 것이라고 생각했습니다. 과연 정신이 멀쩡한 과학자라면 자기가 그렇게 먼 미래까지 내다볼 수 있다고 말할 수 있을까요?

하지만 그러다가 이것이 교육자들이 항상 하는 일과 정확히 일치한다는 사실을 깨달았습니다. 교육자들은 교육 과정을 설계할 때 무엇을 가르치고 무엇을 무시할지를 과감하게 결정하는데, 무려 40~50년 후에도 살아갈 사람들을 위해 그런 일들을 하고 있는 것이었습니다.

앞으로의 반세기에 걸친 컴퓨터 과학에 대한 몇 가지 비전은 이미 진행중이기도 합니다. 다만, 내가 갖고 있는 미래를 보는 수정구슬이 너무 흐릿하기 때문에 세부적인 것들을 이야기하지 못한다는 점을 말해두고 싶습니다. 예를 들어 35년 전의 나는 프로그램 설계와 증명의 설계가 얼마나 밀접하게 연관되어 있을지에 대해 전혀 감이 없었습니다. 그리고 그런 세밀한 것들은 내 삶에 많은 놀라움을 안겨주었습니다.

동시에 이런 놀라움들은 내가 기다려온 진보이기도 했습니다. 왜냐하면 나는 프로그래밍이 어떤 종류의 수학 분과가 될 지 알게 되기 훨씬 전부터 프로그래밍을 일종의 수학적 처리가 가능한 노력으로 바꿔야 한다는 것을 알고 있었기 때문입니다. 다시 말하자면, 이런 것은 해변에서 모래성을 쌓을 때 파도 하나하나는 무시해도 그만이지만, 조류는 무시하면 안 된다는 것과 같은 이치입니다.

Fortunately, there are a few things that we can learn from the past, for instance that the rate at which society can absorb progress is strictly limited, a circumstance that makes long-range prediction a lot easier. Earlier this decade I was told of a great invention called "the register window"; my spokesman was very young, but in my ears the invention sounded very familiar because I remembered the Burroughs B5000 of 30 years before. So, if you have a bright and sound idea now, you can expect it to be hailed as a novelty around the year 2025.

다행히도 우리가 과거로부터 배울 수 있는 것들이 몇 가지 있습니다. 예를 들어 사회가 진보를 받아들이는 속도에는 엄격한 한계가 있어, 이로 인해 장기적인 예측이 쉬워집니다. 10년 전, 나는 "레지스터 윈도우"라는 훌륭한 발명에 대해 들은 바 있습니다. 그것을 내게 설명해준 사람은 아주 어렸지만 나는 30년 전의 Burroughs B5000을 기억하고 있었기 때문에, 그 발명의 내용이 매우 익숙하게 들렸습니다. 따라서 지금 영리하고 타당한 아이디어를 갖고 있다면 2025년 무렵에는 꽤나 참신한 아이디어로 인정받을 수 있을 것입니다.

Another thing we can learn from the past is the failure of characterizations like "Computing Science is really nothing but X" where for X you may substitute your favourite discipline, such as: numerical analysis, electrical engineering, automata theory, queuing theory, lambda calculus, discrete mathematics or proof theory. I mention this because of the current trend to equate computing science with constructive type theory or with category theory.

과거로부터 배울 수 있는 또 다른 교훈은 "컴퓨터 과학은 결국 X일 뿐이다"와 같은 언급들이 실패했다는 것입니다. 여기서 X는 수치 해석, 전자 공학, 오토마타 이론, 큐잉 이론, 람다 계산법, 이산 수학, 증명 이론과 같이 자기가 좋아하는 학문으로 대입할 수 있습니다. 내가 이것을 언급하는 이유는 컴퓨팅 과학을 구성 타입 이론이나 범주 이론과 동일시하는 최근의 경향 때문입니다.

Computing's core challenge is how not to make a mess of it. If people object that any science has to meet that challenge, we should give a double rebuttal. Firstly, machines are so fast and storage capacities are so huge that we face orders of magnitude more room for confusion, the propagation and diffusion of which are easily inadvertently mechanized. Secondly, because we are dealing with artefacts, all unmastered complexity is of our own making; there is no one else to blame and so we had better learn how not to introduce the complexity in the first place.

컴퓨팅의 핵심 과제는 어떻게 해야 엉망으로 만들지 않느냐는 것입니다. 만약에 사람들이 그것은 과학이 해결해야 할 과제가 아니라고 반대한다면, 우리는 두 가지 반론을 할 수 있습니다.

• 첫째, 머신의 속도가 빠르고 저장 용량이 방대하기 때문에, 혼란을 야기하는 요소가 지수적으로 늘어납니다. 이런 혼란은 기계화되어 쉽게 확산 전파됩니다.
• 둘째, 우리는 인공물을 다루고 있기 때문에 우리가 통제하지 못하는 모든 복잡성은 결국 우리 스스로가 만든 것입니다. 우리 외의 누구를 탓할 수 있겠습니까? 우리는 애초에 복잡성을 도입하지 않는 방법을 배워야 합니다.

The history of the real-time interrupt is in this connection illuminating. It was invented for the purpose of facilitating processor sharing; its effect was the introduction of nondeterminism and endless headaches for many an operating systems designer. We have seen two reactions to it. For the purpose of debugging IBM built special-purpose monitors that exactly recorded when the central processor honoured which interrupt; when something had gone wrong, the monitor could be turned into a controller, thus forcing a replay of the suspect history and making the "experiment" repeatable. The other reaction was to determine the conditions under which one could feasibly and safely reason about nondeterministic programs, and subsequently see to it that those conditions were met by both hardware and software. OS/360 was a mess forever after; the THE Multiprogramming System, in contrast, was so robust, that no system malfunctioning ever gave rise to a spurious call for hardware maintenance. Needless to say, the whole episode has made a lasting impression on me.

이러한 맥락에서 실시간 인터럽트의 역사를 살펴볼 수 있겠습니다. 실시간 인터럽트는 프로세서 공유를 용이하게 하기 위해 발명되었지만, 그 결과로 비결정성이 도입되어 많은 운영체제 설계자들에게 끊임없는 골칫거리를 안겨주게 되었습니다.

우리는 이에 대한 반응으로 두 가지를 보았습니다.

• IBM에서는 디버깅을 위해 중앙 프로세서가 어떤 인터럽트를 언제 처리했는지 정확하게 기록하는 특수 목적의 모니터를 만들었습니다. 문제가 발생하면 모니터를 컨트롤러로 전환해서 의심스러운 기록을 강제로 재생해서 "실험"을 반복할 수 있게 한 것입니다.
• 또 다른 반응은 비결정론적 프로그램에 대해 실현 가능하고 안전하게 추론할 수 있는 조건을 먼저 결정한 다음, 하드웨어와 소프트웨어 양쪽에서 그 조건이 충족되는지 확인해보는 것이었습니다.

'IBM의 OS/360'은 그 이후로 영원히 엉망이 되었습니다. 반면 후자를 채택한 'THE Multiprogramming system'¹은 매우 강력해서 시스템 오작동으로 인해 하드웨어 유지보수를 요청하는 일이 거의 발생하지 않았습니다. 말할 필요도 없이 이 사건들은 저에게 깊은 인상을 남겼습니다.

One moral is that the real-time interrupt was only the wave, whereas the tide was the introduction of nondeterminism and of system invariants as a means of coping with it. A wider moral is the constructive approach to the problem of program correctness, to which we can now add the problem of system performance as well. It is only too easy to design resource-sharing systems with such intertwined allocation strategies that no amount of applied queuing theory will prevent most unpleasant performance surprises from emerging. The designer that counts performance predictability among his responsibilities tends to come up with designs that need no queuing theory at all. A last, and this time fairly recent, example is the design of delay-insensitive circuitry, which delegates all timing difficulties in clocked systems to the class of problems better avoided than solved. The moral is clear: prevention is better than cure, in particular if the illness is unmastered complexity, for which no cure exists.

여기에서 얻을 수 있는 한 가지 교훈은 '실시간 인터럽트'는 그저 작은 '파도'에 불과했던 반면, 실시간 인터럽트에 대처하기 위해 도입했던 비결정성과 시스템 불변식은 '조류'였다는 것입니다. 그리고 더 넓은 시야에서 보면, 이로 인해 프로그램의 정확성 문제에 대한 건설적인 접근법이 적용 가능하게 되어, 우리는 이제 시스템 성능 문제까지 해결할 수 있게 되었습니다.

복잡하게 얽힌 할당 전략을 가진 리소스 공유 시스템을 설계하는 것은 꽤 쉬워 보이지만, 실제로는 대기열 이론을 아무리 적용해도 예상치 못한 성능 문제가 발생하는 것을 막기 어렵습니다. 그런 반면, 성능 예측 가능성을 중요하게 생각하는 설계자는 대기열 이론이 전혀 필요 없는 설계를 만들어내는 경향이 있습니다.

최근의 한 예로, 클럭 시스템의 모든 타이밍 문제를 '해결'하는 대신 그 문제를 '회피'하려는 방식의 시도가 있습니다. '지연에 민감하지 않은 회로'라는 설계의 도입이 바로 그것입니다.

예방이 치료보다 낫다는 것은 분명한 교훈입니다. 특히 치료법이 없는 통제 불가능한 복잡성이라는 병에 걸렸을 때는 더욱 그렇습니다.

The above examples point to a very general opportunity, in broad terms to be described as designs such that both the final product and the design process reflect a theory that suffices to prevent a combinatorial explosion of complexity from creeping in. There are many reasons to suppose that this opportunity will stay with us for a very long time, and that is great for the future of computing science because, all through history, simplifications have had a much greater long-range scientific impact than individual feats of ingenuity.

위의 예시들은 '복잡성의 조합적 폭발을 방지하는 이론'을 반영하는 설계라는 매우 중요한 가능성을 보여줍니다. 이러한 설계는 최종 제품뿐만 아니라 설계 과정에도 적용되는 것입니다.

이런 가능성은 앞으로도 우리와 오랫동안 함께할 것으로 예상합니다. 그리고 그것은 여러 이유가 있겠지만 가장 중요한 것은 단순화의 힘이라 할 수 있습니다. 이는 컴퓨팅 과학의 미래에도 큰 도움이 될 것입니다. 역사적으로 보면 단순화는 개별적인 창의력보다 훨씬 더 큰 과학적 영향을 장기적으로 끼쳤기 때문입니다.

The opportunity for simplification is very encouraging because, in all examples that come to mind, the design process cost much less labour and led to a much better final product than its intuitively conceived alternatives. The world being what it is, I also expect this opportunity to stay with us for decades to come. Firstly, simplicity and elegance are unpopular because they require hard work and discipline to achieve and education to be appreciated. Secondly we observe massive investments in efforts that are heading in the opposite direction. I am thinking about so-called design-aids such as circuit simulators, protocol verifiers, algorithm animators, graphical aids for the hardware designer, and elaborate systems for version control: by their suggestion of power, they rather invite than discourage complexity. You cannot expect the hordes of people that have devoted a major part of their professional lives to such efforts to react kindly to the suggestion that most of these efforts have been misguided, and we can hardly expect a more sympathetic ear from the granting agencies that have funded these efforts: too many people have been involved and we know from past experience that what has been sufficiently expensive is automatically declared to have been a great success. Thirdly, the vision that automatic computing should not be such a mess is obscured, over and over again, by the advent of a monstrum that is subsequently forced upon the computing community as a de facto standard (COBOL, FORTRAN, ADA, software for desktop publishing, you name it).

단순화의 가능성은 매우 희망적입니다. 왜냐하면 떠오르는 모든 예시에서, 이러한 설계 과정²은 직관적으로 상상한 대안들보다 훨씬 적은 노력을 들이고, 훨씬 더 나은 최종 제품을 만들어냈기 때문입니다. 나는 이러한 가능성이 앞으로 수십 년 동안 우리와 함께할 것이라고 예상합니다. 세상이 어떤 곳인지를 알기 때문입니다.

• 첫째, 단순함과 우아함은 인기가 없습니다. 이것들을 달성하고 인정받으려면 열심히 노력해야 하고 교육이 필요하기 때문입니다.

• 둘째, 우리는 단순함과는 반대 방향으로 가려는 노력에 대한 대규모의 투자를 목격하고 있습니다. 회로 시뮬레이터, 프로토콜 검증기, 알고리즘 애니메이터, 하드웨어 디자이너를 위한 그래픽 도구, 그리고 버전 관리를 위한 복잡한 시스템과 같은 설계 도구들을 생각하면 됩니다. 이들은 강력하다는 것을 암시하는 방식으로 복잡성을 더욱 끌어올리는 경향이 있습니다. 이런 노력에 전문가로서의 인생 대부분을 바쳤던 사람들이, 이런 것들이 잘못되었다는 말에 친절하게 반응할 거라고는 기대할 수 없습니다. 그리고 이런 것들에 자금을 지원한 기관들에게서도 더 공감하는 반응을 기대할 수도 없겠지요. 너무 많은 사람들이 참여했고, 충분히 큰 돈을 쏟아부은 것이라면 어쨌든 성공한 것으로 알아서 선언된다는 것을, 우리는 과거 경험을 통해 알고 있습니다.

• 셋째, 자동 컴퓨팅이 그렇게 복잡하지 않아야 한다는 비전은 신생 기술의 출현에 의해 매번 반복적으로 흐려져 버립니다. 이들은 컴퓨팅 커뮤니티에게 사실상의 표준으로 강요되었습니다(COBOL, FORTRAN, ADA, 데스크톱 출판 소프트웨어 등).

In short, the opportunity to simplify will remain with us for many years, and I propose, in order to maintain our sanity and enthusiasm, that we welcome the long duration of that opportunity, rather than to suffer from impatience each time the practitioners deride and discard our next successful pilot project as a toy problem: they will do so, even if you have achieved what, shortly before, they had confidently predicted to be impossible.

요약하자면, 단순화의 기회는 앞으로 수십 년 동안 우리와 함께할 것이고, 나는 우리의 정신과 열정을 유지하기 위해, 실무자들이 우리의 다음 성공적인 시제품을 장난감 같다고 조롱하고 쓰레기통에 버릴 때마다 조바심에 시달리기보다는 그 기회가 오래 지속될 것을 즐기는 것을 제안합니다.

얼마 전까지만 해도 불가능하다고 자신있게 말했던 것을 우리가 달성하게 되더라도, 그들은 계속 그렇게 할 것이기 때문입니다.

* * *

By now we all know that programming is as hard or as easy as proving, and that if programming a procedure corresponds to proving a theorem, designing a digital system corresponds to building a mathematical theory. The tasks are isomorphic. We also know that, while from an operational point of view a program can be nothing but an abstract symbol manipulator, the designer of a program had better regard the program as a sophisticated formula. And we also know that there is only one trust-worthy way for the design of sophisticated formulae, viz. derivation by means of symbol manipulation. We have to let the symbols do the work, for that is the only known technique that scales up. Computing and Computing Science unavoidably emerge as an exercise in formal mathematics or, if you wish an acronym, as an exercise in VLSAL (= Very Large Scale Application of Logic).

이제 우리 모두는 프로그래밍은 증명만큼 어렵거나 쉽다는 것을 알고 있습니다. 그리고 만약 프로시저를 프로그래밍하는 것이 정리를 증명하는 것에 해당한다면, 디지털 시스템을 설계하는 것은 수학적인 이론을 구축하는 것에 해당한다는 것도 알고 있습니다. 이 두 작업은 구조적으로 같습니다.

또한 우리는 '운영 관점'에서 보면 프로그램은 '추상적인 기호 조작기'에 불과할 수 있지만, 프로그램 설계자는 프로그램을 '정교한 공식'으로 생각하고 접근하는 것이 더 낫다는 것도 알고 있습니다. 그리고 우리는 정교한 수식을 설계할 때의 신뢰할 수 있는 유일한 방법이 '기호 조작을 통한 유도'뿐이라는 것도 알고 있습니다. 기호가 작업을 수행하도록 만들어야 하는데, 이는 유일하게 알려진 확장성을 가진(scales up) 기술이기 때문입니다.

컴퓨팅과 컴퓨팅 과학은 필연적으로 형식 수학의 연습이라 할 수 있습니다. 약어로는 VLSAL(= 매우 큰 규모의 논리 적용) 연습이라 할 수도 있을 것입니다.

Because of the very close connection between program design and proof design, any advance in program design has a direct potential impact on how general mathematics is done. Since the time computing scientists have built compilers, they are very used to the idea of mechanical manipulation of uninterpreted formulae, and I am sure that they will significantly contribute to a further realization of Leibniz's Dream of presenting calculation, i.e. the manipulation of uninterpreted formulae, as an alternative to human reasoning. The challenge of turning that Dream into reality, however, will certainly keep us busy for at least five decades.

프로그램 설계와 증명 설계는 매우 밀접한 관련이 있기 때문에, 프로그램 설계의 진보는 일반적인 수학의 수행 방식에 직접적이면서 잠재적인 영향을 끼칩니다.

컴퓨팅 과학자들은 컴파일러를 만들 때부터 해석되지 않은 공식을 기계적으로 조작하는 아이디어에 매우 익숙합니다. 그리고 인간의 추론에 대한 대안으로 계산, 즉 '해석되지 않은 공식의 조작을 제시하고자 했던 라이프니츠의 꿈'을 실현하는 데 크게 기여할 것이라고 확신합니다.

그 꿈을 현실로 바꾸는 도전은 최소한 앞으로 50년 동안의 우리를 바쁘게 할 것입니다.

It is not only that the design of an appropriate formal, notational, and conceptual practice is a formidable challenge that still has to be met; it is worse because current traditions are hardly helpful. For instance, we know that the transition from verbal reasoning to formal manipulation can be appreciated as narrowing the bandwidth of communication and documentation, whereas in the name of "ease of use" a lot of effort of the computing community is aimed at widening that bandwidth. Also, we know that we can only use a system by virtue of our knowledge of its properties, and, similarly, pay the greatest possible care to the choice of concepts in terms of which we build up our theories: we know we have to keep it crisp, disentangled, and simple if we refuse to be crushed by the complexities of our own making. But, obviously, the market pulls in the opposite direction. I still remember finding a book on how to use "Wordperfect 5.0" of more than 850 pages, in fact a dozen pages more than my 1951 edition of Geord Joos, "Theoretical Physics"! It is time to unmask the computing community as a Secret Society of the Creation and Preservation of Artificial Complexity. And then we have the software engineers, who only mention formal methods in order to throw suspicion on them. In short, we should not expect too much support for the computing community at large. And from the mathematical community I have learned not to expect too much support either, as informality is the hallmark of the Mathematical Guild, whose members —like poor programmers— derive their intellectual excitement from not quite knowing what they are doing and prefer to be thrilled by the marvel of the human mind (in particular their own ones). For them, the Dream of Leibniz is a Nightmare. In summary, we are on our own.

적절한 형식적, 표기법적, 개념적 관행을 설계하는 것은 여전히 해결해야 할 엄청난 과제입니다. 그런데 그 뿐만 아니라 현재의 전통이 거의 도움이 되지 않기 때문에 더 큰 문제라 할 수 있습니다. 예를 들어, '언어적 추론'에서 '형식적 조작'으로의 전환은 커뮤니케이션과 문서화의 '폭'을 좁히는 것이라 할 수 있는데, '사용 편의성'이라는 명목으로 행해지는 컴퓨팅 커뮤니티의 많은 노력들은 그 '폭'을 넓히는 것을 목표로 한다는 것을 우리는 잘 알고 있습니다. 또한, 우리는 시스템의 속성에 대한 지식이 있어야만 시스템을 사용할 수 있다는 것을 알고 있으며, 마찬가지로 우리가 만든 복잡성에 짓눌리지 않으려면 '이론을 구축하는 개념'의 선택에 최대한 주의를 기울여야 한다는 것도 잘 알고 있습니다.

하지만 시장이 이런 것과 반대 방향으로 움직인다는 것은 명백해 보입니다. 나는 850페이지가 넘는 "워드퍼펙트 5.0" 사용법 책을 본 것을 아직도 기억하는데, 이건 사실 내가 1951년에 읽은 Geord Joos의 "이론 물리학"보다도 수십 페이지가 더 두꺼운 책이었습니다! 이제 인공적인 복잡성을 창조하고 보존하는 비밀 결사가 바로 '컴퓨팅 커뮤니티'라는 숨겨진 진실을 드러낼 때가 되었습니다. 그리고 형식적 방법에 의심을 불러일으키기 위해 그것들을 언급하는 소프트웨어 엔지니어들도 있습니다. 즉, 우리는 전반적인 컴퓨팅 커뮤니티에게서 너무 많은 지원을 기대하면 안 됩니다.

나는 수학 커뮤니티에서도 너무 많은 지원을 기대하지 않는 것이 좋다는 것을 배웠는데, 아마 비공식성이 강한 수학 길드의 특징 때문일 것입니다. 수학 길드의 회원들은 서툰 프로그래머처럼 자신이 무엇을 하고 있는지 잘 모르는 데서 지적 흥분을 얻고 인간 정신의 경이로움(특히 자신의 정신)에 감격하는 것을 선호하기 때문입니다.

그들에게 라이프니츠의 꿈은 악몽입니다. 결국, 우리는 스스로 해결해내야만 합니다.

But that does not matter. In the next fifty years, Mathematics will emerge as The Art and Science of Effective Formal Reasoning, and we shall derive our intellectual excitement from learning How to Let the Symbols Do the Work.

그러나 그것은 중요하지 않습니다. 앞으로 50년 안에 수학은 효과적인 형식적 추론의 예술이자 과학으로 부상하게 될 것이며, 우리는 기호를 작동하도록 하는 방법을 배우는 데에서 지적 흥분을 얻게 될 것입니다.

Calculemus!

계산합시다!³

Edsger W. Dijkstra

(Note. The above is an adapted version of EWD1051.)

주석