Formal Verification: History and Methods

In the first part of our series about formal verification, we discuss the roots of formal verification in fields such as mathematical logic and theoretical computer science.

Upstream posts

Incomplete and Utter Introduction to Modal Logic, Pt. 2

In the first part, we introduced the reader to basic modal logic. In this part of the introduction to the modal logic, we observe use cases and take a look at connections of modal logic with topology, foundations of mathematics, and computer science.

Incomplete and Utter Introduction to Modal Logic, Pt. 1

Modal logic covers such areas of human knowledge as mathematics (especially topology and graph theory), computer science, linguistics, artificial intelligence, and philosophy. Explore this branch of logic together with Danya Rogozin.

Insane Properties of the Closed Long Ray and the Long Line

In topology, the long line, or Alexandroff line, is a space somewhat similar to the real line, but ‘longer’. To obtain the long line, one needs to put together a long ray in each direction. Closed long rays, as well as long lines, have remarkable properties.

Parsing Typed eDSL

Embedded DSL (or eDSL) is a popular technique for encoding your domain specific language into Haskell’s type system. One example of such DSL is Ivory – eDSL for C code generation. Even more often it’s useful to implement your DSL as a Haskell data type and interpret it right from Haskell.

Independent Functions or How to Create the Worst Random Number Generator

Random numbers are used in cryptography, and most of the cryptographic operations use computers. But a computer is a deterministic device, thus, it isn’t able to simply generate a truly random number. There are different approaches to solving the problem, and some of them are worse than others.

The Problem of Intermediate Recursively Enumerable Turing Degrees

The Turing degree of a set of natural numbers is a concept from computer science and mathematical logic that is a measure of the level of algorithmic unsolvability of the set. This post carries you deeper into the problem of the undecidable languages and the halting problem.

Editor’s pick

The Greatest Challenge of Modeling Large Quantum Computers

Perhaps you cannot quite picture how quantum computers work, but you definitely heard something about them. Nowadays, all rich, as well as not-so-rich states and corporations, are trying to build one. However, many face a problem of inability to emulate a large quantum computer. Let us figure out why.

Upstream posts

Trees that Melt: Use of AVL Tree in Blockchains

In modern blockchains, if some node wants to verify a block, it either has to be a full node storing the whole network state, or it has to continuously ask some remote storage for various parts of it. Each of these solutions possesses either inconveniences (storing 100+ GB of data) or risks (the storage forging the data it sends you).

Introduction to Tagless Final

Recently, my team decided to implement an eDSL using the tagless final style for one of the new projects..

Constructive and Non-Constructive Proofs in Agda (Part 3): Playing with Negation

In the previous post, we briefly introduced the reader to dependently typed programming and theorem proving in Agda. Now we present an empty type to work with constructive negation. We discuss Marko…

Constructive and Non-Constructive Proofs in Agda (Part 2): Agda in a Nutshell

Last week, we started a new blog series to introduce you to creating constructive and non-constructive proofs in Agda..

Constructive and Non-Constructive Proofs in Agda (Part 1): Logical Background

Hi! I’m Danya Rogozin, and I work at Serokell on a blockchain framework called Snowdrop.. I would like to tell you about constructive and non-constructive proofs in a proof assistant and functional …

Close