이 세상엔 재밌는게 ㅈㄴ게 많은데

컴공 학문중에서도 ㅈㄴ게 재밌는 학문이 하나 있다


아마 석박한 노예들은 들어는 봤을거다

formal-verification (정형검증) 이라는 아주아주아주 재밌는 학문이 있다

한국에서 해당 학문을 전공하는 연구실은 2개인가? 3개인가? 로 알고 있고 제대로 하는 곳은 한 곳말고는 없다고 알고 있다


사실상 수학에 더 가까운 학문이지만

프로그래밍 언어 이론을 전공하였다면 아마 자기도 모르게 썻을 것이다


초간단하게 말하자면

코드를 수학적 검증을 하는 것이다


이게 대체 뭔 개소린가 싶은데

말 그대로다.


모든 코드는 state-machine으로 나타낼 수 있는데(low level에서)

이를 수학적으로 검증하는 학문이다.


아마 비전공자들은 씨발 뭔개소리를 하는지라고 생각할수도 있어서 조금 사족을 붙이면

1학년때 선형대수랑 공학수학을 때면, 대충 학부 2학년 2학기나 3학년쯤 오토마타 이론을 배우게 되는데 

여기서 state-machine과 튜링이론을 배운다


비전공자라면 꼭 찾아서 배워보길 바란다 존나 재밌는 부분이다

잠깐 딴소리를 조금더 하자면 커리큘럼이 대부분


선대 + 회로기초(논리회로) -> 알고리즘/오토마타/컴퓨터구조론 -> DB/네트워크/OS


이렇게 올라간다


알고리즘과 오토마타가 병행되는 이유는 위에서 말한 튜링이론 때문인데

만약 너가 알고리즘시간에 졸지 않았고 마지막 수업까지 쫒아갔다면

CLRS의 마지막인 P-NP 증명 문제까지 도달 했을 것이다


그리고 p-np를 배우면서 왜 그래프끼리는 제한상태에서만 비교가 되는지를 이해 했을 것이다

그리고 튜링이론도 같이 배웠을 것이다. state는 그래프다. 어떤 느낌인지 알겠지?


여기까지 배웠다면 오토마타 강의중에 model checking을 교수님이 언급을 하셨을 것이다

아마 언급만 하셨을 것이다. 정형검증은 이 model checking을 극한까지 끌어 올린것이라고 생각하면 편하다

비유를 하다보니 자꾸 약간 핀트가 어긋나는 것 같은데, 어찌 되었든 formal-verification은 model checking으로 시작한다고 생각하면 된다


물론 튜링이론하고 p-np 문제는 약간 다른데

어찌 됐든 내가 하고싶은 말은

우리가 짠 코드를 수학적 검증을 할 수 있다는 이야기다


그래서 씨발 이걸왜 공부하는데

이걸 왜 사용하고 어디다 사용하는데?

궁금할텐데


간단하게

시스템이 버그가 없이 완벽하게 동작한다면(완벽하게 수학적으로 증명 되었다면)?

여러분은 어떤 분야에서 가장 먼저 쓸거같은가?


현재 formal-verification에 관련된 가장 활발한 기관은 NIST와 DoD다. 무슨말이냐고? 전투기에 들어간단 소리다

전투기에 왜 들어감? 하는 비전공자를 위해

전투기에도 OS가 들어가는데 그중 RTOS(Real Time Operating System)가 들어간다

그리고 RTOS를 formal-verification 을 이용하여 검증한다


그다음 가장 많이 쓰이는 부분은 어디냐

바로 프로토콜이다. 프로토콜 설계에 이 학문이 굉장히 많이 쓰인다


일단 프로토콜 이라는 주제 하나만으로도 책한권이라 1편에선 여기까지만 하자

어찌 되었든 formal-verification 에 관한 간략한 설명으로 1편을 마친다


관심이 생긴다면

Isabelle/HOL 이나 Z(zed; 제드라고 읽음) language를 한번 찾아보길 바란다