Hey! My name's Kirill Ziborov and I'm a member of the Distributed System Security team at Positive Technologies. In this article, I'll be continuing the discussion of methods and tools for the formal verification of smart contracts and their practical application to prevent vulnerabilities. The main focus will be on the deductive verification method, or more precisely, the ConCert framework for testing and verifying smart contracts.
Rust's type system is quite powerful as it allows to encode complex relationships between user-defined types using recursive rules that are automatically applied by the compiler. Idea behind this post is to use some of those rules to encode properties of our domain. Here we take a look at Peano axioms defined for natural numbers and try to derive some of them using traits, trait bounds and recursive impl blocks. We want to make the compiler work for us by verifying facts about our domain, so that we could invoke the compiler to check whether a particular statement holds or not. Our end goal is to encode natural numbers as types and their relationships as traits such that only valid relationships would compile. (e.g. in case we define types for 1 and 3 and relationship of less than, 1 < 3 should compile but 3 < 1 shouldn't, that all would be encoded using Rust's language syntax of course)
Let's define some natural numbers on the type level first.
When you start learning a programming language(or just programming in general), usually there are first few chapters in books that introduce us such thing like data types (or just types). And we don't focus on this subject as much as we should because it's so simple, right? Well… I think that there is one little detail which can lead to big mistakes of understanding what really data type is.
Recently I wrote an article What is Reactive Programming? iOS Edition where in a simple way I described how to build your own Reactive Framework, and helped you to understand that no-one should be scared by the reactive approach. The previous article could now be named How to cook reactive programming. Part 0., since this is a continuation. I would recommend reading the previous article if you are not familiar with the reactive programming concepts.
In this article, I would like to propose an alternative to the traditional test design style using functional programming concepts in Scala. This approach was inspired by many months of pain from maintaining dozens of failing tests and a burning desire to make them more straightforward and more comprehensible.
Even though the code is in Scala, the proposed ideas are appropriate for developers and QA engineers who use languages supporting functional programming. You can find a Github link with the full solution and an example at the end of the article.
In my previous article I described how to achieve the "Maybe" monad behavior using async/await operators. This time I am going to show how to implement another popular design pattern "Reader Monad" using the same techniques.
That pattern allows implicit passing some context into some function without using function parameters or shared global objects and it can be considered as yet another way to implement dependency injection. For example:
class Config { public string Template; }
public static async Task Main()
{
Console.WriteLine(await GreetGuys().Apply(new Config {Template = "Hi, {0}!"}));
//(Hi, John!, Hi, Jose!)
Console.WriteLine(await GreetGuys().Apply(new Config {Template = "¡Hola, {0}!" }));
//(¡Hola, John!, ¡Hola, Jose!)
}
//These functions do not have any link to any instance of the Config class.
public static async Reader<(string gJohn, string gJose)> GreetGuys()
=> (await Greet("John"), await Greet("Jose"));
static async Reader<string> Greet(string name)
=> string.Format(await ExtractTemplate(), name);
static async Reader<string> ExtractTemplate()
=> await Reader<string>.Read<Config>(c => c.Template);
Generalized async return types — it is a new C#7 feature that allows using not only Task as a return type of async methods but also other types (classes or structures) that satisfy some specific requirements.
At the same time, async/await is a way to call a set of "continuation" functions inside some context which is an essence of another design pattern — Monad. So, can we use async/await to write a code which will behave in the same way like if we used monads? It turns out that — yes (with some reservations). For example, the code below is compilable and working:
async Task Main()
{
foreach (var s in new[] { "1,2", "3,7,1", null, "1" })
{
var res = await Sum(s).GetMaybeResult();
Console.WriteLine(res.IsNothing ? "Nothing" : res.GetValue().ToString());
}
// 3, 11, Nothing, Nothing
}
async Maybe<int> Sum(string input)
{
var args = await Split(input);//No result checking
var result = 0;
foreach (var arg in args)
result += await Parse(arg);//No result checking
return result;
}
Maybe<string[]> Split(string str)
{
var parts = str?.Split(',').Where(s=>!string.IsNullOrWhiteSpace(s)).ToArray();
return parts == null || parts.Length < 2 ? Maybe<string[]>.Nothing() : parts;
}
Maybe<int> Parse(string str)
=> int.TryParse(str, out var result) ? result : Maybe<int>.Nothing();Further, I will explain how the code works...
We’re excited to announce that Visual Studio 2019 will ship a new version of F# when it releases: F# 4.6!
F# 4.6 is a smaller update to the F# language, making it a “true” point-release. As with previous versions of F#, F# 4.6 was developed entirely via an open RFC (requests for comments) process. The F# community has offered very detailed feedback in discussions for this version of the language. You can view all RFCs that correspond with this release here:
This post will detail the feature set and how to get started.
In this article I'm going to tell you about one of the currying options and partial application of the functions in C++ which is my personal favourite. I'm also going to show my own pilot implementation of this thing and explain the point of currying without complex mathematical formula, making it really simple for you. We'll also see what's under the hood of kari.hpp library which we'll be using for currying functions. Anyway, there are lots of fascinating stuff inside, so welcome!