나는 adhd와 우울증을 앓고 있는 기계공학도야.
아이디어가 끊임없이 떠오른다는 것과
이 분야 저 분야 조금씩 파는 것은
adhd 특징이야.
1학년 때 교필로 C언어를 들었는데,
너무 재밌어서 오목도 만들고 네모로직 푸는 것도 만들고, C언어도 심도있게 공부하다가,
나만의 프로그래밍 언어를 만들어보고 싶어졌어.
객체지향 패러다임을 이해하기 위해 C++도 공부해보고,
함수형 패러다임을 이해하기 위해 lambda calculus도 공부했어.
그런데 lambda calculus를 공부하는데 모르는 기호가 나와서 검색해봤더니, 수리논리학에서 나온 기호더라고.
그리고 curry-howard isomorphism도 알게 됐는데,
이것 역시도 수리논리학을 알아야 하더라고.
그래서 정주희 교수님의 저서 "수리논리와 집합론 입문"을 사서 읽었어.
이 책을 고른 이유 중 하나는 proofmood라는 증명보조기를 써서 증명을 확인할 수 있기 때문이었어.
책을 다 읽고 나도 증명보조기를 만들고 싶어졌어.
정확히 말하면 객체지향 함수형 프로그래밍 언어를 만들고, 그것을 해석하는 프로그램(인터프리터)에 추론규칙을 읽고 증명을 확인할 수 있는 기능을 넣고 하고 싶어. 이게 내 인생목표야.
일단 나만의 언어로 1계논리의 추론 규칙들을 작성해봤는데, 맞았는지 틀렸는지 확인 받고싶어.
포기하고 싶은데, 목표가 눈 앞에서 아른거려.
내 능력 밖인 건 아는데, 20년 정도 노오력하면 될 것 같아.
님들의 의견을 듣고 싶으니까, 댓글 많이 달아주세요.
아이디어가 끊임없이 떠오른다는 것과
이 분야 저 분야 조금씩 파는 것은
adhd 특징이야.
1학년 때 교필로 C언어를 들었는데,
너무 재밌어서 오목도 만들고 네모로직 푸는 것도 만들고, C언어도 심도있게 공부하다가,
나만의 프로그래밍 언어를 만들어보고 싶어졌어.
객체지향 패러다임을 이해하기 위해 C++도 공부해보고,
함수형 패러다임을 이해하기 위해 lambda calculus도 공부했어.
그런데 lambda calculus를 공부하는데 모르는 기호가 나와서 검색해봤더니, 수리논리학에서 나온 기호더라고.
그리고 curry-howard isomorphism도 알게 됐는데,
이것 역시도 수리논리학을 알아야 하더라고.
그래서 정주희 교수님의 저서 "수리논리와 집합론 입문"을 사서 읽었어.
이 책을 고른 이유 중 하나는 proofmood라는 증명보조기를 써서 증명을 확인할 수 있기 때문이었어.
책을 다 읽고 나도 증명보조기를 만들고 싶어졌어.
정확히 말하면 객체지향 함수형 프로그래밍 언어를 만들고, 그것을 해석하는 프로그램(인터프리터)에 추론규칙을 읽고 증명을 확인할 수 있는 기능을 넣고 하고 싶어. 이게 내 인생목표야.
일단 나만의 언어로 1계논리의 추론 규칙들을 작성해봤는데, 맞았는지 틀렸는지 확인 받고싶어.
포기하고 싶은데, 목표가 눈 앞에서 아른거려.
내 능력 밖인 건 아는데, 20년 정도 노오력하면 될 것 같아.
님들의 의견을 듣고 싶으니까, 댓글 많이 달아주세요.
본문 내용은 포기하는게 맞는건가?라는 질문을 구체화시키고 있지 않은데
내 인생목표를 포기하는 게 맞을까?
인생 긴데, 뭐 벌써 20년 짜리 목표 세우고 혼자 피곤해하냐 차근차근 공부해보고 목표도 수정해가며 사는거지.
조언 감사합니다. 이게 정답 같네요.
수학갤에서 호응이 없는 이유는 증명보조기를 수학과에서 일반적인 수학을 할때 안쓴다는거... 컴공과에서 우리는 컴파일러를 만듭니다! 하고 한학기동안 세명 숙식시키는게 의미있는거랑 상황이 좀 다른거지 컴파일러는 다 쓰니까.
둘째로 그러면, 저걸 만들면 이런걸 할수있어요. 하는게 자기가 직접 별로 사용자그룹도 없는 언어를 배워서 써야한다는건데.. 프로그래밍 언어만 해도 다른사람에게 자기 언어를 쓰게 하지 못해서 나가 알려준 그 Rust갤도 Rust 보급률 좆망이고 Python 문법 베껴써도 Julia 보급률 좆망이고 한데 그거 사람들이 배우려고 할까? HoL만 해도 그런게 있는지 첨 들어본 애들도 많을건데
그럼 그걸 다 감안해도 그냥 난 자기만족으로 이걸 만들겠다.. 할수 있는데 그러기엔 현재 알려져있는 지식들에 대해 이해도가 높은거 같진 않아보인단 말이지. 그래도 요즘 쓴 글엔 오토마타 이여기도 나오긴 하던데, 저걸 달성하기 위해선 수학적인게 필요한게 아니라 계산복잡도가 얼마나 떨어져야 하는지를 봐야하는데, 너가 대충 적었더뉴이런이런 아이디어로 하겠단건 아무리봐도 수학과에서나 먹힐 논법이지 계산가능한 범위를 벗어나고 있거든. 모든 명제의 참 거짓을 어떻게 주어진걸로 하고싶은거같은데 상식적으로 그런 탐색은 양자컴퓨터라도 안쓴담엔 불가능하잖아.
아 그건 버렸어요. 저도 그건 답이 없는 거 알고 있어요 ㅋㅋㅋ.
뭐 관심을 끌고싶으면 오늘은 튜링의 original paper를 읽었다. 니들이 computable number가 뭔지 알아? P대 NP 풀러간다.ㅅㄱ 이런걸로 어글 끄는게 더 낫다고 봄..
조언 감사합니다. 그러니까 할 거면 그냥 아무것도 바라지 말고 자기만족 선에서 하라는 거죠? 저는 제가 하는 게 유사수학인지 아닌지가 궁금해서 확인 받고 싶어요. 그런데 아무 반응도 없어서 ㅠㅠ.
좀더 정확히 말하면 유사수학인지 아닌지도 모르는 상태. 그걸로 뭐가 재밌는게 없으니 관심이 없음. 예를들면 전에 모치즈키가 10년동안 Paper 쓸땐 사람들이 그냥 단순히 관심이 없다가 이걸로 abc풀었다니 읽는거랑 비슷한? 아직 언어 스펙도 안나왔는데 평가할 수 있는게 없잖아.
전에 문법 설명 올렸다가 비추 먹고 삭제했어요 ㅋㅋ.
아니면 증명보조를 하겠다면 난 자연어를 Butterfly든 뭐든 다른걸로 바꾸는 엔진을 만들겠다던가.. Butterfly로 작성한걸 인간이 읽기 좋은 증명으로 만들겠다던가.. 뭔가 유인책이 있을 떡밥을 던지면 관심이 있을지도. 근데 그건 그냥 왜 Butterfly 쓰냐는 문제엔 답을 안줄거같고
잘 작동하는지 궁금하면 Proof of concept로 잘 알려진 정리들 몇개를 그걸로 증명해본다던가. (라그랑즈 네 제곱수 정리같은거) 대부분 다른 증명보조기도 무슨 formal proof를 넣어 만들지 않거든
그렇군요. 조언 진심으로 감사합니다.
해당 댓글은 삭제되었습니다.
알겠습니다.... 조언 감사합니다.
그런데 제가 만들고자 하는 건 그냥 추론규칙을 읽고 증명이 맞았는지만 확인하는 처리기 뿐인데, 그렇게 어려운 게 필요하나요?
사실 제가 만들려고 하는 건 별 거 아닙니다. 그냥 추론 규칙 or_i :: (Hyps |- A::true) → (Hyps |- or(A, B)::true)를 읽고 사용자의 or_i가 맞았는지 확인하는 프로그램을 만드는 거에요. 여기에 함수형 언어의 인터프리터 기능을 추가한 게 다예요.
coq 같은 건 제 능력 밖임을 잘 알고 있습니다. 그냥 추론규칙의 적용이 올바른지만 확인하는 프로그램이 목표이고 이건 아무도 안 한 거 같아서 해볼려고요.
Coq를 쓸 때 추론규칙을 적을 필요는 없지만, 제 프로그램을 쓸 때는 먼저 추론규칙을 적어야 해요. 이 ㅈ밥 프로그램을 Coq 같은 위대한 프로그램과 동일선에 놓아주신 건 감사한데, 이 정도는 20년 동안 노오력하면 만들 수 있지 않을까요?
알겠습니다. 감사합니다.
이걸로 돈이나 학위나 명예를 바라는 건 아니므로 너무 경계하지는 말아주세요. 그냥 재밌어서 하는 거에요.
알겠습니다. 앞으로 자제하겠습니다. 상담해 주셔서 감사합니다.
나이 몇살이냐 그렇게 미래에 대해 계획 있는것만으로도 요즘 애들이랑은 많이 다르네
22이요. 사회 복무 중임 ㅋㅋ.
근데 니 글 읽어보면 시작부터 너무 먼곳까지 바라보면서 생각하고 걱정하는데 걍 그쪽에 흥미 있으면 해보는게 나쁘지않은듯 그러면서 하는 도중에 시행착오 겪으면서 더 할지 말지 판단 서는거고 일단은 쭉해보는게 그러면서 배우는거 있을거라고 생각됨 그리고 22살에 사회복무중인데 그런거 하는거면 더더욱 좋을듯 그시기 의미 없이 보내는 새끼들 차고 넘침
감사합니다. 이게 정답인 것 같네요.