빅터 태일린이 공개한 Bend, 증명으로 AI 실수를 막고 GPU에서 124배 빠르게 실행

리포에 커밋이 하나뿐이던데 컴파일러는 대체 어디 있는 거임?

bend2/comp.ts에 있음. 런타임이랑 한 파일에 뒤섞여 있어서 예쁘진 않고 gambiarra랑 AI slop이 좀 많다고 하더라. 읽을 거면 커널인 bend.ts를 보라는 게 기여자 말임

Victor Taelin이 만든 HVM 보고 interaction combinator를 컴파일 타겟으로 연구 중인데, Marc Thatcher 박사논문이 interaction net을 곱셈 선형논리의 증명망으로 설명 잘 해놨더라

리포 히스토리를 커밋 1개로 날린 건 좀 심하다. 기여자 44명에 PR 머지한 사람만 41명인데 그 기록이 다 사라졌잖아. AI 시대엔 신뢰가 화폐인데 그렇게 지우면 의심만 커짐

커밋 히스토리에 개인정보랑 AI slop이 잔뜩 있었음. 그게 문제냐?

형식 검증이 답이라고는 안 본다. 페이스북을 어떻게 형식 검증하냐. 당분간은 테스트랑 코드 훑어보기로 갈 듯

AWS Nitro 격리, Apple CoreCrypto, Microsoft Rust 검증 사례 보면 실전에서도 쓰이더라

문제는 law도 내가 바이브코딩해야 하고 그 law가 틀릴 수 있다는 거임

law 자체는 단순하게 쓰고, 그게 성립한다는 증명을 에이전트가 책임지는 구조라고 봄. law가 복잡해질수록 그 보장도 약해지겠지만

자기가 '벽 제거' 예제 해봤는데 결과가 무서웠다고 함. '이길 수 없다' 법 하나만 있으니 AI가 이동을 대각선으로 바꾸는 식으로, 문자는 맞고 정신은 틀린 해법을 냈다더라

Ada/SPARK랑 비교하면 어떤지 궁금함

저자 본인 등장해서 제목 바꿔달라고 하고, 1년 동안 하루 16시간 주 7일 작업했다고 함

설치 스크립트에 sudo가 필요하더라. 여러 번 요구함. 이유는 안 알려줌

가이드에 !가 뭔지 설명이 없음. 같은 코드가 CPU 프로그램이자 GPU 커널이라는 문장이 무슨 뜻인지 모르겠음