형식논리학 공부하면서,
프로그래밍도 같이 공부하는 수갤러임.
Typescript 라고 웹 개발에 엄청 많이 쓰이는 언어가 있는데,
그거 공부하다가 익숙한 단어를 발견함.
'Soundness'
응? 뭐지? 내가 아는 그 건전성인가? 해서 클릭해 봤는데,
맞음.
링크: https://www.typescriptlang.org/play/?strictFunctionTypes=false&q=136#example/soundness
내가 이해한 내용을 요약해보면:
- Type theory 를 모르면, type system 이 "sound" 하다는 게 무슨 의미인지 잘 모를 것이다.
- "Soundness" 란, 컴파일러가 판단한 어떤 값의 type 과, 실제 프로그램을 실행했을 때 그 값의 type 이 일치한다는 것을 보장한다는 것이다.
즉, 이게 성립한다는 의미지? 따라서 위의 type system 이 sound 한 것이고.
(컴파일러의 코드 분석 프로그램) ⊢ "여길 지나는 값의 타입은 모두 T로 추론된다"
⇒
(코드를 기계어로 번역한 프로그램) ⊨ "여길 지나는 값의 타입을 체크해보니, 정말 모두 T이다"
님은 코딩이 실생활임?
코딩 결과물은 실생활임. 요즘 웹페이지 안 보는 사람 없잖아.
시비거는 건 아닌데 그렇게 따지면 그 어떤 전문분야도 실생활이라 할 수 있지 않니. 의료 연구 논문도 병원 안 가는 사람 없으니 실생활이고 양자역학도 실생활에서 쓰는 물질에 관련된거니 실생활이니. - dc App
어떤 이론을 기반으로 개발된 상품이 현재 대중적으로 쓰이고 있다면, 나는 그 이론이 현재 실생활에 쓰인다고 생각함.
어떤 의학 이론을 기반으로 하는 기술이 현재 병원에서 널리 쓰인다면, 그 의학 이론은 현재 실생활에 쓰인다고 생각함. 만약 아니라면, 그 의학 이론은 '현재는' 실생활에 쓰이지 않는다고 생각함.
양자역학 이론의 일부는, 현재 PC 및 스마트폰 CPU를 만드는 기술의 기반 이론에 포함되어 있음. 따라서 일부 양자역학 이론은 현재 실생활임.
프언론 재밌음 - dc App
프언론이 '프로그래밍 언어론'의 줄임말이야? 이런 학문이 있는지도 몰랐네. 덕분에 알았다.
형식논리학은 뭐로 공부함?
https://forallx.openlogicproject.org/
이걸로
독학중임