최근 조합론 증명에 활용되는 Flag algebra 강연을 듣고, 조합론 박사님께 물어보니 자신은 그것도, 또한 Lean도 쓰지 않는다고 했다. 솔직히 전산에서는 AI가 수학에서 뭐든지 할 수 있다는 그런 분위기가 있고 그에 맞춰 AI수학대학원도 생기고 있는데, 선배는 무덤덤한 것이다. 왜냐면 그걸 쓰는 쪽은 자기 증명이 맞는지 불안한 쪽에서 쓰는 것이고 조합은 그렇지 않다는 것이다. 증명하는 건 무조건 좋은 것임에도, 품이 많이 들기 때문에 귀찮을 것이다. 퍼징도 사실 우리가 커밋을 할 때마다 의심지점을 직접 힌트를 준다던가, 정적분석기가 중간에 오류를 내서 뻗으면 절대 고치고 싶지 않고 그냥 넘기고 싶을 것이다. AI 바이브 코딩도 매번 사람한테 물어보고 또 하다가 뻑나고 귀찮지 않은가. 이런게 없이 매끄러울 때 비로소 제대로 usable할 것이다. 이 때 가장 중요한 게 정적분석기이다. 정적분석이 아니 ㄴ다른 부분은 매우 간단하지만 정적분석이 여러 가지 오류의 가짓수를 늘린다. 즉 완전한 정적분석기가 있어야 한다. 어떤 게 중요할까? 하나, 가능한 모든 피쳐가 동작되어야 한다. 내가 C에다가 C++ 코드를 좀 덧댔는데 , 다루지 않은 opcode라고 오류가 나면 안될 것이지만, 현재는 미구현 부분은 에러나도록 되어 있다. slicing을 위해서라면, 구현이 안된 부분은 좀더 간단하게 넘길 수 잇어야 한다. 둘, 너무 분석이 오래걸릴 경우 넘길줄 알아야 한다. 현재 오래걸리는 부분의 이유는 pre-processing이나, implicit call의 가짓수가 너무 많아 처리가 오래걸리는 경우다. inlining이랑, constant propagation으로 해결하고 있으며 이는 ..