본문으로 건너뛰기

위키 홈

일기, 기술/프로그래밍, HCI/UX/디자인, 철학/윤리, 기타 등등 생각나는 거 아무거나 쓰는 개인 위키. 방문을 환영합니다 :)

일지

2026-11-11

형식 증명으로 뭘 할 수 있는지 계속 실험 중이다. 예를 들면 타워디펜스 장르의 게임에서 “모든 전투는 유한 이산시간 안에 끝난다”의 반례 찾기 같은 걸 시킬 수 있다.

  • 스턴 타워(적을 잠시 멈춤)+힐러(스스로 치유하는 적) 조합 탓에 적이 영원히 멈춘 상태로 치유하며 안 끝나는 경우 발생.
  • 목적지에 도달한 적이 플레이어에게 데미지를 입하고 출발지에서 다시 나타나게 하는 메커닉과 플레이어의 치유 메커닉이 공존하면, 특정 상황에서 타워를 몽땅 제거했을 때 게임이 안끝난다. 타워가 없으니 적이 죽지 않고 플레이어가 입은 데미지는 적이 다시 돌아오는 사이에 회복된다.
  • Endurance 모드에서 플레이어의 성장이 적의 성장보다 빠르게 만드는 메커닉이 존재하면 게임이 안끝난다 등등.

“전투는 유한 시간 내에 끝나야 한다”와 같은 불변값들(invariants)을 정의하고 이걸 거스르는 메커닉이 존재하지 않는걸 증명하는 게 가능하다. 물론 불변값 증명만으로는 한계가 있고 시뮬레이터로 기본적인 난이도 조절은 해야하지만, 시뮬레이터와 불변값 증명은 아주 상보적이고 좋은 조합인 것 같다. 장난감 프로젝트로 이런 실험들을 해보며 감을 잡는 중.

한편, Lean 4처럼 증명과 구현을 같은 언어로 할 수 있는 상황이 아니라면 증명과 코드 사이의 불일치를 어떻게 막을 것인지가 중요한 문제 중 하나인 것 같다. specdown에서는 co-location으로 실수 가능성을 좀 줄여보려는 시도를 했으나 말 그대로 실수를 줄일 뿐 근본적인 해결책은 아니다. 오늘 AI랑 얘기를 해보니 구현 언어에서 작고 핵심적인 로직만 커널로 잘 분리하고 이 커널만 증명 언어로 자동 번역하는 방식으로 증명-구현 일부를 연결하는 방식이 종종 쓰인다고 하길래 해보라고 시켜봤다.

2026-11-06

Pandoc의 확장 문법을 도입해서 위키 문서 간 관계에 타입을 부여할 수 있게 하고, 각 타입에 속성(reflexive, transitive, symmetric)을 정의할 수 있게 하고 간단한 추론기를 구현했다.

2026-11-02

약 6개월간 에이전트만 써서 개발한 프로젝트의 소스 코드를 열어봤는데 오물이 엄청 쌓여 있다. 대청소를 한 번 하며 교훈을 좀 얻을 수 있으면 좋겠다.

i-LaTeX: Manipulating Transitional Representations between LaTeX Code and Generated Documents을 읽었다. 지금 내가 만들고 있는 편집기와 매우 유사하다. LLM에게 편집기와 관련된 연구의 역사 및 계보를 알려달라고 Deep research를 시켰다가 발견. 2022년 연구.

2026-10-31

CorTeX 만들며 편집기의 캐럿 이동에 대해 이런저런 고민을 하고 있다. 고민의 중간 결과로 글을 하나 썼다:

2026-10-27

요즘은 CorTeX 라는 학술 글쓰기 서비스를 열심히 만들고 있다.

2026-10-11

결국 옵시디언 대용으로 쓸 뭔가를 만들었다. 폴더를 지원하지 않고 태그가 없고 속도가 빠르면 좋겠어서. 만든지 이틀만에 이제 옵시디언을 더이상 쓰지 않게 됐다. 이게 가능한 이유 중 하나는 내가 옵시디언의 플러그인을 거의 쓰지 않고 있었기 때문인 것 같다.

2026-09-30

정신없이 여러 프로젝트를 하다 보니 위키 관리를 소홀하게 하게 됐다.

2026-09-01

에이전트에게 전력 사용량을 최적화해달라고 했더니 알아서 다양한 문제들을 잡아줬다. 예:

  • 앱은 지웠는데 앱과 함께 설치된 LaunchDaemon이 살아남아서 10초마다 계속 재시작을 시도하며 반복되던 문제를 고쳐서 하루 8,640회 실행되던 프로세스를 제거.
  • ghostty의 커서 블링크가 비정상적으로 배터리를 많이 먹는 문제(cursor-style-blink = false, shell-integration-features = no-cursor)를 고쳐서 유휴 상태 CPU 사용을 22.8%에서 2.4%로 낮춤.
  • tmux statusline이 5초마다 sudo powermetrics(gpu.sh) + ps -A(cpu.sh) + vm_stat(ram.sh)을 스폰하던 문제를 수정. tmux-status.c를 만들고 호출하는 API도 바꾸고 호출 패턴도 최적화해서 유휴 전력 사용량을 78% 낮춤.

2026-08-22

계속 이것저것 개선 중. 이제 SvelteKit 3를 적용해봐야겠다.

내 작은 노트북 하나에도 이렇게 비효율이 많은데 세상엔 고칠 게 얼마나 많이 남아 있을까.

2026-08-18

계속 디자인 조금씩 만져보는 중. 심미안이 없으니 진도가 나가질 않는다. 훈련이 필요한데 좀처럼 뭘 안 한다. 참 게으르기도 하지.

2026-08-15

위키 디자인을 개선했다. 제목에 대해 광학 정렬을 적용하고, 본문 텍스트는 양끝 맞춤을 했다. 되도록 어절이 끊어지지 않도록 했으나 완전히 막지는 못했다. 참고: 2026-08-16 위키 디자인 개편.

지난 일지

2026년:

그 전:

더 옛날:

위키 지도

위키 탐험을 위한 지도 (작업 중)