Pyrofex

To put it very simply, the purpose is to develop software with provable correctness, fault tolerance and security using a category theoretic model of computation and programming. In particular, the goal is to do this in the context of distributed systems, where byzantine fault tolerance is a typically desirable property.

I’m not affiliated with Pyrofex, but I’m working on research in applied category theory and cryptography, and I’m familiar with Mike Stay’s publications. Category theory is broadly applicable to both programming theory and distributed systems, especially in the context of deterministic state machines.

RChain is an Ethereum competitor. It aims to fix several problems with Ethereum.

First, it will scale better: Ethereum currently runs every contract on every computer running a node, and insists on a total order on all transactions. RChain will have a notion of a rooted directed acyclic graph of regions in which contracts will run, a much finer-grained notion of transaction, and will only insist on a partial order for transactions: when they do not conflict, they can be in any order.

Second, Ethereum has no type system. This has led to bugs in various contracts and wallets. In June 2016, a buggy contract led to the theft of $50M in ETH from the DAO. The Ethereum community split into two parts: the first part insisted that "code is law" and that the hacker engaged in a series of perfectly valid transactions with the contract, so he was entitled to the ETH; the second part wanted human intervention to roll back a large transaction that was obviously a bug. They never reconciled, and "Ethereum Classic" forked off as a separate currency. Last year, someone exploited a bug in a Parity wallet and locked up $380M. Contracts are expressions of programmer intent, but programmers are human and make mistakes. Type systems allow programmers to write a kind of "summary" of their intent as a type. The compiler compares the two expressions and fails if they are not consistent. Greg Meredith (President of RChain) showed that one could have defended against the theft using a spatial-behavioral type system: https://docs.google.com/document/d/1sGlObhGhoEizBXC30Ww4h1KH...

Third, the Ethereum VM has suffered from various bugs (https://bounty.ethereum.org/) and relies on a find-and-patch system. RChain intends to formally verify as much of the platform as possible.

Last and probably least, Ethereum uses proof of work, which is basically proof of stake, but you're staking GPUs and ongoing electricity costs. RChain will use Vlad Zamfir's "correct by construction" proof of stake algorithm.

-- Mike Stay

Your comment may be spot-on, if you don't tell me why it's useful, I won't care one whit.

Maybe but this is a mathematician's blog, so perhaps you are not the intended audience.

Could you try looking at it as at an art piece?