Lưu ý của biên tập viên: Bài viết này đến từ Lưu ý của biên tập viên: Bài viết này đến từPhòng thí nghiệm Ambi SECBIT

(ID: SECBIT), tác giả: Guo Yu, người sáng lập SECBIT Lab, được phát hành với sự cho phép.

Trong lĩnh vực blockchain, không có giải pháp nào áp dụng các phương pháp truyền thống sẽ chiến thắng và chỉ có sự đổi mới mới có tương lai.

——Quách Vũ

Tôi tin rằng tất cả mọi người, giống như tôi, đã được tối đa hóa bởi vòng kết nối bạn bè trên Facebook ngày hôm nay.

Libra, dự án tiền kỹ thuật số mã hóa do Facebook khởi xướng, đã chính thức ra mắt vào ngày hôm nay (18/6). Libra đồng thời phát hành một trang web chính thức đa ngôn ngữ và sách trắng, định vị mình là cơ sở hạ tầng dịch vụ tài chính và tiền tệ toàn cầu cho hàng tỷ người. Libra cũng đã phát hành một số sách trắng kỹ thuật trình bày chi tiết về ngôn ngữ lập trình mới được phát triển Move và giao thức đồng thuận LibraBFT. Mã nguồn Libra đã được mã nguồn mở trên GitHub và mạng thử nghiệm cũng đã được khởi chạy. Hiện được thiết kế dưới dạng chuỗi được phép (chuỗi tập đoàn), nó tuyên bố rằng không có giải pháp trưởng thành nào cho chuỗi không được phép hiện tại (chuỗi công khai) có thể hỗ trợ nhu cầu của hàng tỷ người và chỉ ra rằng quá trình chuyển đổi sang chuỗi không được phép chuỗi sẽ bắt đầu trong vòng năm năm sau khi phát hành Công việc.

Trong số các bản phát hành của Libra, ngôn ngữ lập trình mới Move đặc biệt bắt mắt. Tôi đọc sách trắng của Move lần đầu tiên, có lẽ đây là ngôn ngữ hợp đồng thông minh sẽ như thế nào trong tương lai.

Their design goals seem to overlap, or even aim to replace Ethereum?

Một nhà phát triển đến từ Berlin, Lefteris Karapetsas, đưa ra quan điểm của mình về các nền tảng xã hội:

Mục tiêu thiết kế của họ dường như hơi trùng lặp hoặc thậm chí họ có ý định thay thế Ethereum?

I think "move" programming language released by $FB could be more interesting than libra.

Theo CryptoPuzzleDream, người sáng lập PuzzleToLife.com:

Tôi nghĩ ngôn ngữ "di chuyển" do FB phát hành thú vị hơn libra.

I'm usually pretty skeptical of anything related to cryptocurrency, but here's one piece of Libra that looks potentially interesting: a bytecode programming language called Move with semantics inspired by linear logic.

James Clark, một người đam mê tiêu chuẩn, cho biết:

Tôi thường hoài nghi về bất cứ điều gì liên quan đến tiền điện tử, nhưng một phần của Libra trông khá thú vị: ngôn ngữ lập trình mã byte có tên Move, có ngữ nghĩa được lấy cảm hứng từ logic tuyến tính.

Move là ngôn ngữ nền tảng hợp đồng thông minh dành cho "tài sản kỹ thuật số".

tiêu đề phụ

Ba công dụng hữu ích của Move Language

• Phát hành tiền kỹ thuật số, Token và tài sản kỹ thuật số

• tiêu đề phụ

Hệ thống kiểu tĩnh từ dưới lên

Hệ thống kiểu tĩnh từ dưới lên

Well-typed programs never get stuck.

Di chuyển sử dụng một hệ thống kiểu tĩnh, về cơ bản là một ràng buộc logic. Nó nghiêm ngặt hơn nhiều so với ngôn ngữ hợp đồng thông minh của Ethereum. Các ngôn ngữ lập trình hiện đại như Rust, Golang, Typescript, Haskell, Scala và OCaml đều áp dụng hệ thống kiểu tĩnh Ưu điểm của chúng là có thể tìm thấy nhiều lỗi lập trình cấp thấp tại thời điểm biên dịch thay vì bị trì hoãn cho đến khi chạy lỗi.

Đây là một thuật ngữ tiếng lóng trong thế giới ngôn ngữ lập trình (PL): một mã đúng kiểu sẽ không bao giờ hết. Có nghĩa là nếu một đoạn mã hợp đồng được kiểm tra kiểu thì độ tin cậy sẽ khá cao.

tiêu đề phụ

Triết lý tài nguyên hạng nhất

Triết lý tài nguyên hạng nhất

Từ tài nguyên hạng nhất khá hàn lâm, trong bản dịch tiếng Trung, tài nguyên là công dân hạng nhất, điều này có nghĩa là gì?

Cái gọi là công dân hạng nhất của ngôn ngữ lập trình là đối tượng lập trình mà ngôn ngữ lập trình xem xét đầu tiên khi lập trình.

Vậy tài nguyên, Tài nguyên là gì? Đó cũng là một cái tên rất hàn lâm. Tài nguyên là một khái niệm tương ứng với Giá trị. Giá trị có thể được sao chép theo ý muốn, trong khi Tài nguyên chỉ có thể được tiêu thụ chứ không thể sao chép. Tài nguyên giống như Coke, uống một chai sẽ mất một chai, còn Giá trị giống như một từ tiếng Anh được viết trong một cuốn sổ, bạn có thể đọc nó mỗi sáng, và nó sẽ không biến mất sau khi đọc, nếu bạn nhớ nó, sau đó Chỉ cần tạo một bản sao trong đầu tôi. Chẳng những chư vị đọc được, tôi cũng đọc được, chư vị đọc thuộc được, tôi cũng đọc được.

Các ngôn ngữ lập trình truyền thống, bao gồm cả ngôn ngữ hợp đồng thông minh Ethereum, áp dụng phương pháp Giá trị để ghi sổ sách tài sản kỹ thuật số, dẫn đến một vấn đề: có thể mắc lỗi trong sổ sách kế toán. Trên thực tế, có khá nhiều hợp đồng thông minh bị ghi sai tài khoản, chẳng hạn như khi Zhang San chuyển tiền cho Li Si, tài khoản của Li Si có thêm 10 nhân dân tệ, nhưng số dư tài khoản của Zhang San không thay đổi. Nhiều lỗ hổng kế toán khác nhau trong hai năm qua thậm chí đã khiến mọi người mất niềm tin vào tương lai của hợp đồng thông minh.

• Hợp đồng Move áp dụng một loại hấp thụ lý thuyết truyền thống về "logic tuyến tính", được gọi là loại tài nguyên. Tài sản kỹ thuật số có thể được xác định theo "loại tài nguyên". Theo cách này, tài sản kỹ thuật số, giống như tài nguyên, đáp ứng một số đặc điểm trong logic tuyến tính:

• Tài sản kỹ thuật số không thể được sao chép

• Tài sản kỹ thuật số không thể biến mất trong không khí

Ý nghĩa thực sự của Tài nguyên hạng nhất là tài sản kỹ thuật số là công dân hạng nhất Câu này có thể được mở rộng với thực tế rằng Move là ngôn ngữ hợp đồng thông minh để vận hành tài sản kỹ thuật số. Từ quan điểm kỹ thuật, tài sản kỹ thuật số có thể được sử dụng làm biến hợp đồng, tài sản kỹ thuật số có thể được lưu trữ, gán giá trị, được sử dụng làm tham số của hàm/thủ tục hoặc làm giá trị trả về của hàm/thủ tục. Và hệ thống kiểu tĩnh của Move cho phép mã hợp đồng thông minh kiểm tra hầu hết các lỗi sử dụng tài nguyên thông qua trình biên dịch trong quá trình biên dịch, tức là trước khi triển khai. Các hợp đồng thông minh được đảm bảo không còn dễ vỡ như trước đây.

Tài nguyên hạng nhất là một khái niệm rất chung mà các lập trình viên có thể sử dụng không chỉ để triển khai các tài sản kỹ thuật số an toàn mà còn để viết logic nghiệp vụ chính xác để bao bọc tài sản và thực thi các chính sách kiểm soát truy cập. sử dụng nó không chỉ để triển khai các tài sản kỹ thuật số an toàn mà còn để viết logic nghiệp vụ chính xác và triển khai các chính sách kiểm soát truy cập chính xác.

tiêu đề phụ

Thiết kế bảo mật hợp đồng

Hợp đồng Move được thiết kế với sự xem xét đầy đủ về bảo mật. Trước hết, Move không hỗ trợ gán động (Dynamic Dispatch). Được rồi, hãy để tôi giải thích Dynamic Dispatch là gì Theo thuật ngữ thông thường, đây là một cơ chế ngôn ngữ rất linh hoạt. Nhiều hàm, thủ tục hoặc chương trình con có thể được viết trong chương trình. Sau đó, một chương trình chính có thể gọi các hàm/thủ tục/chương trình con này để hoàn thành các chức năng khác nhau tương ứng. Nếu chương trình đang chạy ta có thể biết nó gọi hàm nào, hoặc gọi nhiều hàm theo một thứ tự nào đó thì các lời gọi hàm này là “tĩnh”, nếu trước khi chạy ta không biết lời gọi hàm của bước nào đó là hàm nào. được gọi, cho đến khi chương trình chạy, chúng ta chỉ có thể biết thông qua quan sát, khi đó lời gọi hàm này được gọi là "động". "Động" rõ ràng là linh hoạt hơn "tĩnh".

Nhưng linh hoạt cũng có nghĩa là dễ gặp vấn đề hơn. Nhiều ngôn ngữ lập trình hiện đại ít nhiều hỗ trợ gán động, tức là hỗ trợ trực tiếp từ cấp độ ngôn ngữ, chẳng hạn như "ràng buộc động" do "kế thừa" gây ra trong các ngôn ngữ hướng đối tượng. Các tính năng động không có lợi cho lập luận chương trình, thậm chí còn ít có lợi cho việc xác minh chính thức (Formal verify), và có nhiều khả năng gây ra các vấn đề về bảo mật. Có nhiều "tính năng động" trong thiết kế hợp đồng thông minh Ethereum, chẳng hạn như hỗ trợ con trỏ hàm dưới dạng tham số, hợp đồng dưới dạng tham số, cuộc gọi ủy nhiệm, v.v. Trong ngôn ngữ Move, nó không hỗ trợ bất kỳ hình thức "gán động" hoặc "tính năng động" nào. Tất cả các đường dẫn thực thi hợp đồng có thể được xác định tại thời điểm biên dịch, sau đó có thể được phân tích và xác minh đầy đủ.

Trước khi hợp đồng Move được chạy, nó sẽ được xác minh bởi một trình xác minh mã byte (Bytecode verifier), có thể kiểm tra nhiều loại lỗi khác nhau. Đồng thời, khi bytecode được giải thích và thực thi, nó vẫn mang kiểu và nó được kiểm tra trong khi chạy.

So với nền tảng Ethereum EVM, hệ thống mô-đun Move không hỗ trợ các phụ thuộc đệ quy vòng tròn, giúp giải quyết hoàn hảo lỗ hổng gia nhập lại hợp đồng (Re-entrancy).

tiêu đề phụ

Hệ thống mô-đun mạnh mẽ

Move modules are similar to smart contracts in other blockchain languages. …, However, modules enforce strong data abstraction — a type is transparent inside its declaring module and opaque outside of it.

Hệ thống mô-đun Move được thiết kế theo kiểu ngôn ngữ lập trình chức năng (OCaml, Coq, SML), theo sách trắng:

Hệ thống mô-đun của Move cung cấp một nền tảng rất tốt để xác minh chính thức các hợp đồng thông minh và "bất biến" có thể được xác định bên trong mô-đun. Cái gọi là bất biến đề cập đến một ràng buộc nghiêm ngặt đối với trạng thái bên trong của tài sản kỹ thuật số, có thể cung cấp thông tin rất có giá trị để tự động hóa xác minh chính thức. Hơn nữa, "sự trừu tượng rõ ràng" của hệ thống mô-đun có thể làm cho việc xác minh chính thức hoạt động theo mô-đun và chi phí thấp hơn. Viết trình phân tích chương trình và trình thực thi ký hiệu trên hệ thống mô-đun Move sẽ đơn giản hơn nhiều, vì sau khi trừu tượng hóa, logic hợp đồng có thể được thực hiện rất đơn giản và dễ suy luận.

chữ

Hợp đồng thông minh Move chứng minh tương lai

Mặc dù Move có vẻ hơi thô và non nớt nhưng hướng đi này vẫn rất thú vị Từ cấp độ ngôn ngữ Move, chúng ta có thể thấy tham vọng trở thành một nền tảng tài sản kỹ thuật số khổng lồ của Facebook. Vai trò này lẽ ra phải thuộc về Ethereum.

• Tại sao tôi lại yêu Move một chút, sau khi nghĩ về nó, có lẽ có ba lý do:

• Nó đã tiếp thu những thành tựu nghiên cứu trong lĩnh vực PL (ngôn ngữ lập trình), đồng thời tiếp thu kinh nghiệm và bài học của ngôn ngữ hợp đồng thông minh EVM

• Thiết kế rất coi trọng "tính chính xác và bảo mật của hợp đồng thông minh"