IT에서의 Formalism(형식주의)
IT를 수학만큼 논리정연하게 만들 수 있을까?
어떤 이론(또는 어떤 설명)을 전개해 나가는 방법이 형식적이고 논리적이면 그 방법은 formal하다고 말합니다. (대체할만한 적당한 우리 나라 말이 생각이 안 나네요) 경험적 사실이나 경험적 개념을 대상으로 하지 않는 과학은 formal science, 형식 과학이라고 합니다. 오토마타 이론은 전산학의 꽃이라 불립니다. 그 이유는 아마도 그 formal한 어찌보면 딱딱하지만, 그러기에 더욱더 논리적인 면 때문일 것입니다. formalism을 제일 잘 보여주는 학문은 역시 수학이죠. 그만큼 정리가 잘 되어 있다는 뜻입니다.
IT에 이 formalism을 적용할 수는 없을까요? 되는대로 하는 기술이 아닌, 잘 정리해서 입증하고, 증명하며 IT를 발전시킬 수는 없을까요? 요즘 새로운 보안기술로 대두되고 있는 IPS. 이것을 과연 수학의 한 분야인 대수학만큼 논리적으로 잘 설명하고, 정리할 수 있을까요? 요즘 많이 되고 있는 웹 어플리케이션 서비스. 이것을 오토마타 이론처럼 formal하게 정리하고 접근할 수 있을까요? (고등학교 때 많이 봤던 수학 "정석"에 보면 수학은 논리적인 사고를 길러주기 때문에 수학을 공부해야 한다고 써있죠. IT에 우리는 논리적인 면(논리적인 방법론)을 얼마나 강조하고 있을까요? 회사에서 기술을 개발한다고 할 때 우리는 논리적인 "정의"와 "증명"을 얼마나 하고 있을까요?)
이런 시도가 되고 있다면, 어떤 방법으로 되고 있나요? 그리고 실제로 얼마나 많이 쓰이고 있나요? 별로 쓰이고 있지 않다면 그 이유는 무엇일까요?
이런 시도가 없다면, 이런 시도가 필요하지 않을까요? 아니면, 이런 시도는 아예 의미없는 것일까요?
저는 이런 시도가 되지 않고 있다고 생각합니다. (제가 알바를 했던 회사가 3군데인데, 이런 시도는 전혀 없었습니다) 하지만 필요하다고 생각합니다. 왠지 논리적이며, 증명된 것이 아니면 가치가 떨어지는 것으로 생각되거든요. IT의 가치를 올리기 위해서 이런 시도는 필요한 것 같습니다.
여러분의 생각은 어떠세요?
겁쟁이가 왜이렇게 많은거야!
겁쟁이가 왜이렇게 많은거야!
문제의 요지를 모르겠습니다.수학은 학문이고 아이티는 산업입니다.즉
문제의 요지를 모르겠습니다.
수학은 학문이고 아이티는 산업입니다.
즉, 전자는 순수고 후자는 응용입니다.
순수는 추상화, 일반화를 지향하고
응용은 특수화, 구체적 적용을 지향합니다.
포멀리즘은 말 그대로 순수, 추상, 일반화의
영역이죠. -_-
formal methods는 소프트웨어 공학의 한 분야를 차지하고 있으며
formal methods는 소프트웨어 공학의 한 분야를 차지하고 있으며
계속해서 활발하게 연구되고 있는 분야 입니다.
아직까지는 academic 한 측면이 많이 있지만, 계속해서 산업계에서 실제적으로
응용하기 위한 많은 시도들이 이루어 지고 있습니다.
우리나라에서는 많지 않지만, 외국에서는 현재 safe-critical 시스템 분야(항공,
방위산업, 원자력, 고속철도, security-protocol...) 에서 많은 응용이 이루어
지고 있습니다 (응용 사례 같은것들이 많이 있어요)
formal methods는 또 여러가지 분야들로 나눠지는데요
formal specification, formal verification 등으로 분류(?) 할 수 있는것 같습니다.
formal specification은 formal specificiation language를 이용해서 작성된
명세(specification) 입니다.
마치 C 프로그램은 C 언어를 이용해서 작성된것이니까...
비슷하다고 할까요...
programming language도 C, JAVA, C# 등등과 같이 계속해서 새로운 언어가 나오고
발전하는것 처럼 formal spec language도 무쟈게 많이 나와 있고, 새로 나오고 있습니다.
크게 sequential, concurrent 분야로 구분해서 보자면
sequential 한 프로그램에서 많이 사용되는 formal spec language는
Z(zed로 읽어요, 제드), VDM, 등등.. (기억이 잘 안나지만 무쟈게 많습니다)
concurrent 한 프로그램에서 많이 사용되는 언어는
CSP, CCS, PETRI-NET(스펠이 맞는지..) 하여튼 이쪽도 무쟈게 많습니다.
각각의 formal spec language마다 syntax, semantics, rules of inference(추론규칙)가
정의되어 있습니다.
그래서 명세를 작성하고 나면 rules of inference를 이용하여 원하는 속성(properties)을
만족하는지 아닌지 검증(verification)해볼수 있습니다.
이것이 의미하는것은 프로그램으로 만들기 전에 원하는 속성들을 증명해볼 수 있다는 것입니다.
이런 과정을 formal verification 이라고 합니다. 더 큰 의미도 있는데....
(이 의미를 자세히 설명하기에는 좀 실력이 부족합니다.)
손으로 일일이 proof(증명)을 하기 힘들기 때문에 interpreter와 유사한 증명을
도와주는 프로그램들이 많이 나와 있습니다. (자동 증명기도 있습니다....)
요즘 미국에서 많이 연구하는 분야가 model-checking 인데... theorem-proving 보다는
조금 쉬운듯한 감이 들기는 하지만 (개인적인 -_-;;) 이론부터 이해하고 tool 을 사용하기
까지 어렵기는 마찬가지인것 같습니다...
참고하실 사이트는 http://www.afm.sbu.ac.uk/ 에 가보시면... 될것 같습니다.
뭔진 모리지만 재미난 내용인거 같군요...물론 겁나게 어려운거 같기도
뭔진 모리지만 재미난 내용인거 같군요...
물론 겁나게 어려운거 같기도 하고요.
그런데 대충 제가 이해한바로는 그러한 것을 사용하는곳은 소위 작업이 겁나게
민감한 것들의 것(사고나면 큰일나는)들 인데, 그러한 것은 돈의 액수와는
상관이 없는 것들 이잖아요? 돈보다는 안전을 생각한다. 절대 오류가 있어선
안된다. 그러한 것에서 출발한것이지 어디 한번 빨리 만들어서 돈을 만들어보자
에서 출발한거 같진 않군요. 물론 더욱더 발전하면 그것이 여러곳에 쓰일지도 모르겠습니다.
허나 지금의 우리 실정은 그러한 것을 적용하기엔 너무 급한거 아닌가요?
한마디로 IT에선 남의 나라 이야기다 이거죠...
-영희-
정형화되고 잘 짜여진 틀이 생기면 더이상 개발자들이 필요없어지죠. 단순한
정형화되고 잘 짜여진 틀이 생기면 더이상 개발자들이 필요없어지죠. 단순한 기능공으로도 충분하니까요. 물론 그 틀을 만드는 사람은 엄청난
대우를 받죠. 하지만 어디 사회 돌아가는 모양새가 그런가요? 정형화된 도구를 이용할만 하면 새로운 개념과 사업영역이 생기는데요. 여전히 구식 틀로 할 수 있는 일은 많겠지만 수익을 얻기 힘들어서 포기하는 경우가 많아지죠.
헉. 수정이나 삭제가 안되는군요. 정형화된 도구의 끝에 기다리는 작업
헉. 수정이나 삭제가 안되는군요. 정형화된 도구의 끝에
기다리는 작업은 온갖 삽질과 예쁘게 꾸미기 작업이 남아
있습니다. 횡설 수설~
시간은 돈이져. IT 분야만을 의미해서 하는 말이 아니에요. 잘 정리되고
시간은 돈이져. IT 분야만을 의미해서 하는 말이 아니에요. 잘 정리되고 정립되는 것. 완벽과 시간은 언제나 반비례 관계에 있고, 완벽하고 깔끔한 것이 언제나 나은 것은 아니져.
하고 싶은 말은 하나 붙들고 세월에 네월아 하는 것이 아닌 짧은 시간안에 완벽하고 깔끔한 결과를 내놓을 수 있는 사람은 많지 않다는 것이져. 그만큼 남보다 뛰어난 두뇌 회전과 그걸 해낼 수 있는 부지런함과 집중력, 여튼 고급 인력이라고 말할 수 있겠져.
Formalism...IT쪽 사람들은 Formal 하지 않다.
Formalism...
IT쪽 사람들은 Formal 하지 않다.
Customer는 더욱 더하다.
Anonymous wrote...> Formalism...>
Anonymous wrote...
> Formalism...
>
> IT쪽 사람들은 Formal 하지 않다.
> Customer는 더욱 더하다.
이것이 바로 유일한 Formal 이다.
수필에 대한 정의를 빌어서 끝에 추가해 보았습니다.
사람은 Formal 하지 않다.
사람이 쓴 수필은 더욱 더하다.
이것이 수필의 유일한 Formal이다.
라고 된 것이었죠.
원래 IT의 기반이 수학과 자연과학의 진보에 따른문명의 이기로 등장한
원래 IT의 기반이 수학과 자연과학의 진보에 따른
문명의 이기로 등장한 기술이라고 볼 때
IT의 바탕은 수학과 과학에 있다고 할 수 있죠.
따라서 IT는 formal이 이미 적용된건 아닌지...
IT라는 것이 H/W, S/W를 포괄할 진데
어떤분야의 개발방법은 아주 포멀한 접근이
유용하겠지만 어떤분야는 비정형적 접근이
더 나은 결과를 얻을 수도 있겠죠.
예를들어, 미래의 프로그램 개발 방법이
지금처럼 포멀한 언어로 작성하는 것이
아니라 인간이 사용하는 자연어로 작성
할 만큼 발달한다라고 본다면
과연 포멀한 것이 필요할런지...
> 예를들어, 미래의 프로그램 개발 방법이> 지금처럼 포멀한 언어로
> 예를들어, 미래의 프로그램 개발 방법이
> 지금처럼 포멀한 언어로 작성하는 것이
> 아니라 인간이 사용하는 자연어로 작성
> 할 만큼 발달한다라고 본다면
> 과연 포멀한 것이 필요할런지...
이렇게 하기위해서, 포멀한것이 꼭 필요하죠
Computer science 에는 수학이 적용되었지만요즘 말하는 I
Computer science 에는 수학이 적용되었지만
요즘 말하는 Information Technology 에는 수학이
적용이 안되있는것 같습니다.
물론 이런 접근방법이 비 효율적일수도 있겠지만
반대로 말하면 효율적일수도 있죠~~^^
특히 기반이 되는 부분이라면...
신뢰성이 있어야 하는데
수학을 기반으로 개발하면 신뢰성을 확보할수 있습니다
(저는 그렇게 믿고 있습니다)
효용곡선 하나 만들어 내려해도 수학이 기본이 되야하죠.그런데 그런
효용곡선 하나 만들어 내려해도 수학이 기본이 되야하죠.
그런데 그런건 그냥 예전에 개발해놓은 수학적인 모델을
컴퓨터로 옮기면 되는데요...
그런데 문제는 고객은 그러한것은 기본으로 된다고 보고,
나머지 귀찮은것을 겁나게 많이 요구하잖아요.
그걸 일일이 맞추다보면 결국 노가다를 해줘야 한다는거죠.
-영희-
글쎄요, 형식주의와 실리주의라는 주제는 아주 오래된 문제인듯하군요.
글쎄요, 형식주의와 실리주의라는 주제는 아주 오래된 문제인듯하군요. 어느쪽 한쪽으로 치우쳐 결정되지는 않을 듯 싶네요. 더욱이 우리나라와 같이 실리와 형식이 적당히 타협하며 진행되는 상황에서는요.
가장 중요한 것은 그 상황에 가장 경제적인 방법을 적용하는 것이 그리고 가장 이상적이라고 판단되는 방법을 적용하는 것이 좋겠네요.
너무 이거다, 저거다 하는것은 수천년간 해온일이니 우리는 수천년의 경험을 바탕으로 판단한다면 그리 어렵지 않게 받아들여질 수 있는 문제인듯 하네요.
뭐 다들 어느정도 알고 계실테지만 검색엔진에서 formal metho
뭐 다들 어느정도 알고 계실테지만
검색엔진에서 formal method 라고 치시면
우리나라 혹은 외국에서 이런쪽으로
연구하고 있는 내용들이 나올것입니다.
저도 이 formal method 를 공부하는 입장이고
저는 아직 내공이 깊지 못해서
많이 알고 있지는 안지만 그래도 같은 분야에
대해서 공부하고 싶어하는 분이 있으니까
기쁘네요~~^^
Formal한 방법은 이미 사용되고 있습니다.다만 그러한 개발 방
Formal한 방법은 이미 사용되고 있습니다.
다만 그러한 개발 방법을 사용하면 개발 비용이
무지하게 올라갑니다... 개발 기간도 길어지고
즉 수지타산이 안 맞아서 일반적인 분야에는
사용이 불가능합니다.
우주선 쏘고 그러는 분야에서는 아주 중요한
부분같은 경우는 formal하게 작성한다고
들었습니다...
동네 꽃집에서 꽃배달하는데 15톤 트럭을
사용하면 비용도 많이 들고, 배달도 늦어져서
망할겁니다...
비용의 문제가 직접적인 것은 아니고 그 내용을 받아들일 수 있는 사람의
비용의 문제가 직접적인 것은 아니고 그 내용을 받아들일 수 있는 사람의
능력이 직접적인 문제입니다. 대부분의 개발자들은 그만한 능력을 가지지
못한 경우가 많습니다. 비행기를 타면 빨리 갈 수 있다는 것을 알지만
겨우 걸어다니는 정도를 하는 사람에게 파일럿이 되라고 할 수는 없겠지요.
그래서 파일럿 흉내라도 낼때까지 계속 돈을 퍼 부어야 되는데... 그러면
이제 배보다 배꼽이 더 커지지요.
반대라고 생각합니다....파일럿은...몇명있지만....회사에서
반대라고 생각합니다....
파일럿은...몇명있지만....
회사에서 비행기를 도입하려하지 않기때문에....
이 비행기라는것의 존재 자체를 일반사람들이 모르는것 아닐까요???
잘못알고 있는건가??? --?
회사에 큰 이익을 주는 것을 반대하는 사람은 거의 없을 것입니다. 게다가
회사에 큰 이익을 주는 것을 반대하는 사람은 거의 없을 것입니다. 게다가
그 비행기라는 것은 아주 저렴하죠(방법론일 뿐이라). 문제는 파일럿이
없다는 것입니다. 그 싼, 아니면 거의 비용이 들지 않는(아 바닥이 다
그렇지만, 가장 비싼 것은 사람입니다.) 비행기를 몰아 갈 수 있는
파일럿이...
model checking 방식을 이용한다면 아주(!) 우수한 인력이 아
model checking 방식을 이용한다면 아주(!) 우수한 인력이 아니라도
어느정도 활용할수 있다고 생각합니다.
물론 model checking 자체의 단점이 있기는 하지만
모델체커는 아주 우수한 일력이 아니라도
활용할수 있다고 생각합니다만..
Model Checking 이라는 것은 어떤 것인가요?
Model Checking 이라는 것은 어떤 것인가요?
제가 허접인지라...아는대로만 말하겠습니다.일단 제가 알고있는 본문의
제가 허접인지라...아는대로만 말하겠습니다.
일단 제가 알고있는 본문의 내용처럼
Formal 하게 정리하는것은..formal method
란 분야로 SE 의 한 분야입니다.
여기에서 제가 아는거는(^^;) 2가지 방식이
있는데 하나는 Model checking 방식과
Theorem Proving 방식이 제가 아는 방식입니다.
더있기는 한데 나머지는 제가 설명
할정도로 아는 것이 아니라서....
Model checking 방식은 시스템을
추상화된 모델로 표현합니다.
보통 FSM 이나 state diagram 등으로
표현 가능합니다.그리고 시스템이
만족해야할 속성을 시제 논리로 표현 하고요.
(속성의예. 클라이언트가 메시지를 보내면
서버는 메시지를 반드시 받아야한다)
그래서 시스템이 속성을 만족하는지 검사하는
방식입니다. 제가 알고있는 툴은 SMV 와 SPIN
을 알고있고요. 뭐 딴것도 있는데 제가 몰라서(^^)
하지만 이것도 실제로 프로그램 검증에 쓰이기에는
아직은 힘들것 같다는것이 제 생각입니다.
주로 많이 쓰인다고 하는곳이 보통 프로토콜 검증
입니다
제가 아는게 없어서
혹시 제말중 틀린점 있으면 리플달아주세요~~
위에 글쓴 사람인데요...참고로...본문에 있는 글 쓴분은...주
위에 글쓴 사람인데요...
참고로...본문에 있는 글 쓴분은...
주로 Formal Specification 에 대해 말한것 같은데..
저는 Formal Verification 에 대해서 말했네요...
둘다 Formal method 분류이지만
다시생각해 보니...제가 엉뚱한거 적었나 해서
글 썼습니다.
전혀 엉뚱하지 않는데여...^^;다만 제 생각에는 말씀하신 어느정
전혀 엉뚱하지 않는데여...^^;
다만 제 생각에는 말씀하신 어느정도 우수한 인력도
드물지않나 생각이 드네여...^^;
이글을 보니까 열심히 공부만 하면 되겠구나하는 생각이 드네요~~~
이글을 보니까 열심히 공부만 하면 되겠구나
하는 생각이 드네요~~~
희망을 주셔서 감사합니다~~~^^
잘은 모르지만 사용자에게 다가가기위해 만드는거 아닌가요? 결국 감성, 인
잘은 모르지만 사용자에게 다가가기위해 만드는거 아닌가요? 결국 감성, 인지쪽의 접근이 중요한데 그걸 형식화 한다는건 조금 이상하네요. 고객은 언제나 움직이잖아요.
언제나 고객 편에서 서비스 제공을 해준다. 그걸 기본으로 해야 할거 같습니다.
-영희-