공부하다가 심심해서 요즘 관심 있는 분야 이야기나 약간. 나도 개론이나 보는 수준이니 정확성은 기대하지 말고 그냥 이런 것도 있구나 정도로 걸러 듣길.


여기 사람들은 거의 철학/수학도이고 수리논리나 수학기초론 쪽에 관심이 있는 듯 한데, 이쪽이 현대 논리학의 뿌리이긴 하지만 그 밖에도 매우 다양한 분과가 있지. 논리학이 가장 활발히 응용되는 분야는 아마 CS일 거고, 최근 들어서는 formal methods에 대한 관심도 높아지는 추세. 정형기법이라고도 하는데, 뭉뚱그려서 말하자면 복잡한 시스템이 제대로 작동한다는 것을 논리적 증명으로 보증하는 기법이라고 생각하면 된다.  컴파일러의 최적화가 termination을 보존한다는 것을 어떻게 장담할 수 있을까? 악성 유저가 암호화폐를 두 곳에서 이중결제할 수 없다는 것은? 과거에는 귀납적으로 다양한 테스트를 돌려 보고 사후에 문제가 생기면 고치는 식으로 대응했지만, 자동화의 경제적 중요성이 커지고 안전한 시스템에 대한 수요가 늘어난 결과, 그런 문제가 발생할 수 없다는 것을 사전에 논리적으로 엄밀하게 증명할 필요가 생긴 거지.


정형기법을 살짝 맛보기 좋은 예시로는 Needham–Schroeder 프로토콜이 있다. 간단히 말해서 엿듣는 침입자를 배제하고 두 사람을 암호화된 채널로 연결시키는 방법인데, 설명(https://en.wikipedia.org/wiki/Needham–Schroeder_protocol)을 보면 암호학을 전혀 몰라도 이해할 수 있을 정도로 원리는 간단함. 언뜻 보기에는 안전해 보이고, 실제로 그 보안의 헛점을 전문가들이 찾아내기까지 17년(!) 이나 걸린 방식이지. 하지만 여기서 침입자의 존재를 시간논리(temporal logic)식으로 표현하고 모델 체커를 돌리면 치명적인 man-in-the-middle 공격을 0.1초만에 발견한다. 논리학의 실용적 위력을 실감할 수 있는 사례인데, 직접 재현해 보는 것도 어렵지 않으니 관심 있는 사람은 https://members.loria.fr/SMerz/papers/mc-tutorial.pdf 이 튜토리얼을 참조하길.


물론 정형기법은 상당한 기술과 시간을 요구하는 방법이기 때문에 아직은 보급에 한계가 있다. 1. 현존하는 논리적 방법론으로 기술/증명이 용이하고 2. 오류 발생시의 손실이 막대한 분야일수록 적극적으로 활용되는 추세인데, 명제논리만으로도 다양한 명세를 표현할 수 있으며 소프트웨어 같은 사후 패치가 불가능한 하드웨어 업계가 대표적이지. 인텔에 수백만 달러의 손실을 안긴 94년의 부동소수점 연산 오류 (https://en.wikipedia.org/wiki/Pentium_FDIV_bug) 등을 보면 그 유용성을 능히 짐작할 수 있는 것이고.


앞으로 정형기법의 최대 프론티어는 아마 사물인터넷이나 자율주행차처럼 물리적 컴포넌트와 결합한 cyber-physical 시스템일 텐데, 이런 물리계를 모델링하기 위해서는 기존의 discrete한 접근으로는 한계가 있음. 따라서 실수 등 연속적 도메인을 다룰 수 있는 logic 및 증명 알고리즘의 연구가 활발하게 진행되고 있는데, 이것이 향후 논리학의 중요한 발전 방향 중 하나가 아닐까 생각된다.