SmartPy.io 的界面如下。屏幕左侧区域是代码编写区，开拓者可以轻松地利用 Python 来写入并编辑合约的代码。Smartpy 不需要像 Remix 一样分两步编译和执行，按一下代码区上方的执行按钮就一步搞定，很是利便。执行功效立马就可以在屏幕右侧显示出来，，包罗合约挪用的进口、存储状态、编译的 Michelson 代码等。
在传统互联网应用中，假如处事器被黑客进攻，只需要对处事器端用户数据举办回滚就可以挽回用户损失。因此，重视用户体验的传统互联网应用可以以牺牲安详性调换速度和成果上的快速迭代。然而在 DeFi 应用中，由于区块链的不行改动性，智能合约一旦上线并呈现安详隐患，对用户造成的损失是庞大且不行挽回的。
形式化验证指的是用数学中的形式化要领对算法的性质举办证明或证伪，要领有两种：
Michelson 语言的安详特性
陈设的智能合约可以用 SmartPy Contract Explorer 举办查察，合约的当前状态和汗青操纵都尽收眼底。
所有进入 Michelson 智能合约的数据，都需要明晰界说其范例。制止了跟范例不匹配有关的措施 bug ，如浮点溢出、除以 0 等。
Cryptoverse Wars: https://cryptocodeschool.in/tezos/overview/
形式化验证要领和 DeFi 安详
DeFi 的发作式增长吸引了不少开拓者，著名的 DeFi 协议如 Compound、Uniswap、Syntheix 累计收获了上亿美元的资金。可是，DeFi 存在一个重大裂痕：安详性。
我们看到，在以上项目中，Tezos 支持的智能合约高级语言的种类最富厚，不只包罗 Pascal, Ocaml, Haskell 等多种函数式语言，也包罗了 Python 这一应用普遍的语言。而 Cardano、Aeternity 都需要开拓者进修一门新的函数式语言，使得开拓门槛变得较高。
很多区块链项目为了担保安详性，在底层架构、虚拟机或智能合约的语言方面，选择了函数式语言，如 Ocaml、Haskell、Erlang 等。函数式语言由于其严格的变量范例界说和编译检讨，以及拥有较好的形式化验证东西链（好比 CoQ ），在安详规模拥有很好的口碑。常见进程式语言编写的代码，一般必需从头用函数式语言标志方能举办形式化验证。
Tezos 上的 Dapp 开拓者并不需要把握 Michelson 语言 。这是因为开拓者可以利用基于 Python 的 SmartPy SDK ，并将 Python 代码写的智能合约编译成 Michelson 语言。因此 Dapp 开拓者只需要会 Python 就可以轻松上手。
Michelson 与 EVM 的主要区别是，
SmartPy 开拓东西包
今朝 SmartPy 已经支持 Python 常见的很多成果，如当地变量，变量范例判定，Lambda 函数等。少数不支持的成果如 array，可以用 map 来取代。这也就意味着进修 SmartPy 不需要投入许多的时间和精神，开拓者可以专注于实现更好的成果。
在智能合约语言的设计上，Tezos 回收了一种取长补短的创新方案。Tezos 的智能合约底层回收基于 Ocaml 的 Michelson 语言，而开拓者实际打仗的是 Python 等高级语言，并不需要相识 Michelson 语言自己。如此以来，可以团结 Michelson 语言更好的安详性与可审计性，与 Python 等高级语言的易于编程性。
Tezos（特所思）作为著名的 PoS 公链，其亮点并不只仅只是 Staking，Tezos 的形式化验证特征同样也是其主要技能亮点之一。形式化验证能让 DeFi 的安详性方面如虎添翼，让用户对资金的智能合约安详越发有信心。
SmartPy是一个Python 库，而 SmartPy.io 让用户可以或许在一个欣赏器中执行 Python 剧本。Smartpy 的官方网站提供了一个在线编辑器(https://smartpy.io/demo/)，Dapp 开拓者可以直接用 Python 编写代码并编译成 Michelson 智能合约，然后陈设到 Tezos 主网上。其利用界面设计对比以太坊的 Remix 在线编辑器更简捷明白，很是容易上手。Smartpy 还自带了一些现成的开拓模版，利便开拓者参考进修。2）原子计较
1）静态范例
函数式语言在公链规模的应用
区块链开拓人员今朝仍然是稀缺的，导致人工审计的本钱很是奋发。因此越来越多地利用呆板帮助验证是今朝的趋势，而呆板帮助审计中的形式化验证要领更是确保安详性的不二瑰宝。
巨细写、空格、短行都有严格类型的要求，让代码审计变得更利便。
另一种是演绎验证，首先把系统代码标志成抽象数学模子，然后对定理举办证明，此种要领适合大型系统，可是首先需要人工将系统的运作要领转换成验证系统可以领略的语言。
以下是一些关于 SmartPy 入门的练习课程：
一个 Michelson 智能合约必需完成执行后才气挪用其它智能合约。这一点制止了以太坊上常常产生的 re-entrancy 进攻 (如著名的 DAO 进攻）。
这个裂痕的价钱是昂贵的，它给一些项目（好比）的网络效应带来了负面的影响。已往几个月被进攻的 DeFi 项目就包罗 Curve.fi、Lendf.Me、PegNet 等，其损失从数十万美元到数千万美元不等。tBTC 在上线几天后通过自查实时发明白 bug 并冻结了存币，制止了一场劫难。
形式化验证要领在很长一段时间里，由于其本钱较奋发，主要应用于学术、国防军工、航空航天等规模，在贸易规模应用较少。由于传统互联网应用与的运行情况有着本质的差异，其开拓流程也该当相应地举办调解，个中最要害点在于安详验证环节的投入比例。
2）利用链上存储
Michelson 在架构上对标的是以太坊 EVM ，与 EVM 对比其相似之处有
可以看到 Michelson 对比 EVM 在安详上有诸多的改造，可以更好地抵制以太坊上常常呈现的进攻范例。
3）明晰的挪用失败
4）严格的语义
Blockmatics SmartPy Developer course: https://cryptocodeschool.in/tezos/overview/1）是一种 stack 语言
4）图灵完备
一种是模子检讨，即把系统所有大概的状态列出并举办一一检讨，此种要领全自动化但只适合小型系统；
郑重声明：本文版权归原作者所有，转载文章仅为传播更多信息之目的，如作者信息标记有误，请第一时间联系我们修改或删除，多谢。
