미켈슨

미켈슨(Michelson)은 테조스(Tezos) 블록체인에 스마트 컨트랙트(Smart contract)를 작성하는데 사용되는 로우레벨(Low-Level) 스택 기반 프로그래밍 언어이다. 미켈슨은 테조스 블록체인에 스마트 계약서를 작성하는 데 사용되는 DSL(Domain-specific langauge)이다. 미켈슨은 스택 기반(stack-based) 언어이며 변수가 없고, 스택 지향(Stack-oriented) 언어는 하나 이상의 스택에서 작동하며 각 스택은 서로 다른 용도로 사용될 수 있다.

개요

미켈슨(Michelson) 프로그래밍 언어는 스택 기반이며 다형성(polymorphism), 클로저(closures), 또는 명명 함수(named function)와 같은 기능이 포함되어 있지 않다. 리퀴디티(Liquidity)라는 고급 프로그래밍을 작성하여 미켈슨(Michelson) 언어로 컴파일할 수 있다. 미켈슨(Michelson)의 언어의 구현은 오카멜(OCaml) GADT를 기반으로 한다. 미켈슨은 테조스 블록체인에 Smart contract를 작성하는 데 사용되는 로우레벨(low-level) 스택 기반(stack-based) 프로그래밍 언어이다. 미켈슨은 사용자가 계약의 속성을 증명할 수 있게하고 형식 검증(formal verification)을 용이하게하기 위해 설계되었다.

스택 rewrite 패러다임을 사용하고 그에 따라 각 함수가 입력 스택을 출력 스택으로 다시 작성합니다. (이에 대한 의미는 밑에서 완전히 설명 할 것입니다.) 이것은 순전히 함수적(functional) 방식으로 실행되고 입력값을 전혀 수정하지 않습니다. 따라서 모든 데이터 구조는 불변(immutable) 합니다.

특징

미켈슨(Michelson)은 손으로 쓸 수 있으며 컴파일러의 출력조차도 이해할 수 있게 한다는 목표로 알아보기 쉽게 설계되었다. 미켈슨(Michelson)을 사용하는 데 있어 두 가지의 중요한 동기가 있다. 첫 번째는 읽을 수 있는 바이트코드를 제공하고, 두 번째는 자신이 잘못된 것이 무엇인지 알 수 있는 것이다. 로우레벨(Low-Level)의 바이트코드에서 프로그램과 컴파일러 툴에 대한 확신이 필요하다. 미켈슨(Michelson)을 사용하면 실행된 프로그램의 속성을 보다 쉽게 검사하고 확인할 수 있다. 미켈슨(Michelson)의 현재 구현은 오카멜(OCaml) GADT를 기반으로 하며 언어의 정확성과 시간을 검증하는 데 사용한다. 또한 스택 기반 언어라 구현은 시멘틱에 직접 매핑된다. 그리고 테조스(Tezos)에서 사용되고 있는 이 미켈슨(Michelson)과 오카멜(OCaml)의 프로그래밍 언어는 빠른 속도와 높은 보안성 구현이 가능하다. 먼저 미켈슨(Michelson)은 세부적인 오류를 잡아내는데 특화된 언어로서 높은 보안성이 가능하다. 오카멜(OCaml)은 짧은 코드로 기능들을 구현할 수 있는 언어이기에 수정이 쉽고 빠르다. 두 프로그래밍 언어는 스마트 컨트랙트의 복잡한 코드를 보다 쉽게 설계한 언어이다.

• 리퀴디티, 미켈슨 차이점

리퀴디티(Liquidity)는 테조스(Tezos)를 위해 개발된 완전 함수형 프로그래밍 언어로 리퀴디티는 테조스에서 Smart contract를 프로그래밍하는 데 사용하는 고급 언어이고 완전 함수형 언어(fully functional language)이며, 리퀴디티는 OCaml의 문법(syntax)을 사용하며, Michelson의 보안 제한을 엄격히 준수한다. 리퀴디티는 100% Michelson의 특색을 가지며, 리퀴디티로 만들어진 계약은 메인 네트워크에 제출 가능하다. 그럼 리퀴디티와 미켈슨의 차이점 으로는 유동성이 있다. 유동성은 Michelson에서 엄격하게 컴파일(compile)된다. (프로그래밍)언어로서 리퀴디티는 문법(syntax), 로컬 변수(local variables) 및 고급 타입(high-level type)을 사용하기 때문에 많은 개발자들이 스택 조작(stack manipulation)보다는 쉽게 접근 할 수 있고 리퀴디티에 대한 형식-검증(Formal-verification) 프레임워크가 개발 중이다.

활용

미켈슨(Michelson) 언어는 스마트 계약의 수학적 코드의 정확성을 검증하는 데 필요한 간단한 트랜잭션의 논리적 프로세스와 시스템의 간단한 관리를 위해 사용된다. 또, 다중 서명 지갑(multi-signal wallets), 권리 부여 및 분배(vesting and distribution)와 같은 사업을 도와주는 데 집중하고 있으며, 이를 다른 언어에 비해 쉽고 누구나 사용할 수 있게 만들어져 있다. 또한, 테조스(Tezos)만의 특징인 스스로 수정해나가는 점과 같이 미켈슨(Michelson) 언어도 천천히 확장해 나가며 기능들을 추가함을 계획하고 있다.

언어

미켈슨 언어{#michelson_KR}

• 미켈슨은 이상한 언어처럼 보이지만, 다형성(polymorphism), 클로저(closures) 또는 명명 함수(named function)와 같은 기능은 포함하지 않는다. 하스겔(Haskell)이나 오캐멀(OCaml) 같은 언어와 비교할 때, 능력이 좀 부족한 것처럼 보이지만, 미켈슨의 스택이 항상 다루기 쉬운 것은 아니며 표준 라이브러리가 없다. 그러나 이러한 제한들은 언어의 디자인 목표에 의해 크게 영향을 받게 되는데, 미켈슨을 사용하는데 있어서 아래와 같은 두가지 주요한 동기가 있다.

1. 읽을수 있는 bytecode를 제공한다.
2. 스스로를 잘못된 것이 무엇인지 알수 있다(To be introspectable).

• 테조스는 Smart contract의 역할에 관해 이더리움(Ethereum)과 약간 다르다. 플랫폼을 일반적인 세계 컴퓨터 보다는 특정 비즈니스 로직을 구현하는 방법으로 생각하고, 이더리움에서 대부분의 계약은 multisig wallet, 토큰 획득권(vesting) 및 배포규칙 같은 것을 구현했는데 미켈슨도 이러한 유형의 어플리케이션을 구현하려고 한다. 메켈슨은 심지어 손으로도 쓸 수 있고 컴파일러의 출력조차도 이해할 수 있게 한다라는 목표로 알아보기 쉬운 컴파일러로 설계 되었으며, 언어는 개발자가 자신의 분석 툴과 컴파일러를 개발자가 원하는데로 만들 수 있도록 간단해야 한다. 이는 EVM의 에서 출발한 것이며, EVM의 바이트 코드는 어셈블리와 매우 유사하다. 로우 레벨의 바이트 코드에서는 프로그램과 컴파일러 툴체인에 대한 확신이 필요하지만, 미켈슨을 사용하면 실제로 실행 된 프로그램의 속성을 보다 쉽게 ​​검사(verify)하고 확인(check)할 수 있다. 고급 바이트 코드를 사용하면 컴파일 출력물에 대한 속성을 증명하는 프로세스가 단순해 지는데, 미켈슨으로 작성된 프로그램은 SMT solver로 적절하게 분석 할 수 있으며 분리논리(Seperation logic)와 같은 더 복잡한 기법을 사용할 필요없이 Coq로 형식화(formalize)된다. 마찬가지로 강제 들여쓰기(indentation)와 대문자 표기법(Capitalization)으로 인한 제한 사항으로 들여쓰기와 정렬 트릭으로 소스를 난독화할 수 없다.

• 미켈슨의 현재 구현은 OCaml GADT를 기반으로 하고 있으며, OCaml GADT는 언어의 타입-적정성을(type-soundness) 검증하는 데 사용된다. 또한 스택 기반 언어의 구현은 시멘틱(의미론, Semantic)에 직접 매핑된다. lambda-calculus를 효율적으로 구현하는 경우에도 그대로 적용되고, 또한 공식적으로 검증된 미켈슨의 구현은 두개가 있는데, 하나는 Coq에, 다른 하나는 F*에 구현되어 있다. 마지막으로, 테조스의 주요장점 중 하나는 시스템이 수정 가능하다(Amendable)는 것이다. 자신 있는 작은 코어 언어로 시작하여 좋은 use case가 만들어지면서 기능을 추가하고자 하고, 시작할때 모든 것을 언어에 담고 이후의 호환성을 깨뜨리고 싶지 않다. 미켈슨은 비즈니스 로직을 위한 간단한 플랫폼을 제공하고, 이해하기 쉬운 바이트 코드를 제공하며, 스스로 잘못된 것이 뭔지 아는것이 가능하도록 하고, 올린 쉬버(Olin Shivers)와 함께 일할 때, 그는 항상 작업을 위한 충분히 작은 도구"를 사용하는 것을 매우 좋아했다. 미켈슨은 그런 도구가 되도록 조심스럽게 설계되었다.

오카멜 언어

미켈슨, 오카멜 언어는 테조스 블록체인에서 스마트계약을 기록하기 위한 언어이다. 두 언어 모두 스마트계약의 코드를 수학적으로 구현하는 데 특화됐으며, 간단한 코드로 설계된 언어인 만큼 수정하기 쉽다. 이 자체 언어들은 수정도 쉽지만 안정적이라는 장점도 있고, 원조 블록체인인 비트코인의 C++언어는 그간 버그(프로그램 오류) 발생 가능성이 있다는 지적을 받았다. 버그가 악용될 경우 블록체인 네트워크가 마비될 수 있기 때문에 보안에도 악영향을 끼치며, 보안이 흔들리는 플랫폼 위에서 디앱들은 안정적으로 구축될 수 없다. 그러나 앞서 말했듯 테조스의 미켈슨, 오카멜 언어는 스마트계약의 코드를 수학적으로 증명하기에 적합며, 이는 보안을 향상시키는 데 이용되는 기술인 공식검증을 가능하게 하고, 버그 발생 가능성을 낮춘다. 디앱들이 보다 안정적으로 자리 잡을 수 있게 되는것이고 테조스가 스마트계약과 디앱(DApp)을 위한 플랫폼을 내세울 수 있는 이유다.

참고자료

• ㈜테조스코리아 공식 커뮤니티 - https://tezoskoreacommunity.org/
• areyoucrazy, 〈테조스의 특징을 초보자의 눈높이에 맞게 이야기해보았습니다.〉, 《스팀잇》, 2018-02-20
• 박현영 기자, 〈(신비한 코인사전)<22> 하드포크 필요 없는 블록체인 '테조스'〉, 《서울경제》, 2018-10-02
• 코인원, 〈(코인원의 코인스낵) 1. 스스로 진화하는 블록체인, 테조스(Tezos)〉, 《네이버블로그》, 2018-10-12
• Skkrypto, 〈(TezosXSkkrypto) 테조스 실습노트 #6〉, 《브런치》, 2019-05-06
• 고영준, 〈Tezos Smart Contracts에 대한 소개 {#faq_KR}〉, 《테조스코리아커뮤니티》

같이보기

• 테조스
• 프로그래밍 언어
• 오카멜
• 리퀴디티

이 미켈슨 문서는 프로그래밍에 관한 토막글입니다. 위키 문서는 누구든지 자유롭게 편집할 수 있습니다. [편집]을 눌러 이 문서의 내용을 채워주세요.

개발 : 프로그래밍 □■⊕, 소프트웨어, 데이터, 솔루션, 보안, 하드웨어, 컴퓨터, 사무자동화, 인터넷, 모바일, 사물인터넷, 게임, 메타버스, 디자인 프로그래밍 언어 ASP • C 언어 • C++ • C# • CSS • D 언어 • HTML • HTML5 • JSP • PHP • R • XHTML • XML • XSLT • 고(Go) • 고급언어 • 기계어 • 델파이 • 러스트 • 루비 • 루아 • 리액트 • 리퀴디티 • 무브 • 미켈슨 • 베이직 • 브이비스크립트 • 비주얼 C++ • 비주얼베이직(VB) • 비주얼베이직닷넷(VB.NET) • 솔리디티 • 스몰토크 • 스위프트 언어 • 스칼라 • 스크립트 언어 • 알골 • 어셈블리 • 언리얼스크립트 • 얼랭 • 에이잭스(Ajax) • 엠에프씨(MFC) • 오브젝티브-C • 오브젝트 파스칼 • 오카멜 • 웹어셈블리(WASM) • 이와즘(eWASM) • 자바 • 자바스크립트 • 저급언어 • 제이슨(JSON) • 제이쿼리(jQuery) • 카멜 • 코볼 • 코틀린 • 콜드퓨전 • 타입스크립트 • 파스칼 • 파워스크립트 • 파이썬 • 펄(Perl) • 포트란 • 프로씨(Pro-C) • 피엘에스큐엘(PL/SQL) • 피엘원(PL/I) • 하스켈 개발방법론 CBD 개발방법론 • EA • 구조적 개발방법론 • 객체지향 개발방법론 • 라이브러리 • 람다 아키텍처 • 모듈 • 모듈화 • 벤치마킹 • 소프트웨어 개발방법론 • 스크럼 • 스프린트 • 아키텍처 • 아키텍트 • 애자일 • 웹개발방법론 • 정보공학 개발방법론 • 컴포넌트 • 테일러링 • 템플릿 • 폭포수 모델 • 프로젝트 • 프로토타입 • 피드백 코딩 EUC-KR • UTF-8 • 값 • 글루웨어 • 디버깅 • 디코딩 • 마크업 • 버그 • 부트스트랩 • 세이브포인트 • 소스코드 • 시큐어코딩 • 아스키 • 액티브엑스 • 오픈소스 • 유니코드 • 인코딩 • 재컴파일 • 주석 • 컴파일 • 컴퓨터 프로그램 • 코드 • 코딩 • 태그 • 테스트 • 테이블 • 텍스트 • 파싱 • 퍼블리싱 • 퓨니코드 • 하드코딩 • 하이퍼링크 • 하이퍼텍스트 프로그래밍 C 명령어 • 객체 • 객체지향 • 객체지향 프로그래밍 • 거짓 • 관계연산자 • 기본형 변수 • 널 • 논리 • 논리연산 • 논리연산자 • 다중상속 • 다형성 • 대입 • 대입문 • 대입연산자 • 더블 • 도스 명령어 • 디폴트 • 레지스터변수 • 루프 • 리눅스 명령어 • 리턴 • 메모리 주소 • 메소드 • 멤버 • 명령문 • 명령어 • 무한루프 • 문자 • 문자열 • 바이트 • 반복문 • 배열 • 변수 • 분기 • 분기문 • 불린 • 브레이크 • 비교연산자 • 비트연산자 • 산술연산자 • 상속 • 상수 • 생성자 • 선언 • 선언문 • 설정자 • 속성 • 스위치 • 스태틱 • 시프트연산자 • 실행 • 실행문 • 어노테이션 • 에코 • 역참조 • 연산 • 연산문 • 연산자 • 오버로딩 • 오버라이딩 • 외부변수 • 윈도우 명령어 • 유닉스 명령어 • 인스턴스 • 인스트럭션 • 인클루드 • 인터페이스 • 임포트 • 입력 • 입력문 • 입출력 • 입출력문 • 자료형(데이터 타입) • 자바 명령어 • 자바 예약어 • 자바 컬렉션 • 전역변수 • 접근자 • 접근제어자 • 정보은닉 • 정수형 • 정적변수 • 제어 • 제어문 • 제어자 • 조건 • 조건문 • 조건연산자 • 주소 • 증감연산자 • 지역변수 • 참 • 참조 • 참조변수 • 초기화 • 추상메소드 • 추상클래스 • 추상화 • 출력 • 출력문 • 캡슐화 • 케이스 • 클래스 • 파라미터(매개변수) • 파이널 • 패키지 • 퍼블릭 • 포인터 • 프라이빗 • 프로텍티드 • 필드(멤버변수) • 함수 • 환경변수 명령어 abstract • array • boolean • break • byte • case • char • continue • default • double • do while • echo • elif • else • else if • false • final • float • for • gosub • goto • if • if else • import • include • int • join • long • long long • null • print • printf • println • private • protected • public • return • scanf • short • stdio.h • static • string • switch • temp • then • true • unsigned • void • while 디자인패턴 구조패턴 • 동시성패턴 • 동시실행패턴 • 모델-뷰-컨트롤러 패턴 • 상태패턴 • 생성패턴 • 싱글톤패턴 • 아키텍처패턴 • 전략패턴 • 커맨드패턴 • 행동패턴 프로그래밍 인물 귀도 반 로썸 • 그레이스 머레이 호퍼 • 니클라우스 비르트 • 댄 브릭클린 • 더그 커팅 • 데니스 리치 • 리누스 토르발스 • 리처드 그린블라트 • 마거릿 해밀턴 • 마크 앤드리슨 • 빈트 서프 • 빌 게이츠 • 빌 조이 • 스티브 잡스 • 에이다 러브레이스 • 제임스 고슬링 • 척 벤턴 • 켄 톰슨 • 팀 패터슨 위키 : 자동차, 교통, 지역, 산업, 기업, 단체, 업무, 쇼핑, 블록체인, 암호화폐, 인공지능, 개발, 인물, 행사, 일반