rwosync

It's pure vapourware, word is that they burnt through their runway hiring a team of overpriced Haskell consultants who just built a new programming language and didn't deliver a product.

> In a way that doesn't involve A16Z cynically mis-representing blockchain as some people's champion.

That's precisely the game for these funds to keep that illusion up. They buy up a bunch of tokens in a presale discount, pump the price, and then dump it to a bunch of foreign retail investors based on inside information before the inevitable failure of the "product". A16z's crypto fund has made a killing doing just this and it's entirely legal. The SEC is only going to go after the founders and a16z will have long exited their position by the time of the lawsuit.

We've gone from 'time to build' back to 'time to build speculative financial products with no utility' pretty fast.

There are likewise some inaccuracies in this post. Both OPs seems to agree on the fact that Libra has no transaction privacy and then pick nits about features not being there at this point in time:

> Libra’s byzantine tolerance on a permissioned network is an incoherent design.

This post's argument rests on their being a unused flag in the configuration file for a feature which is not implemented. The Libra whitepaper indicates that a permissionless design is beyond their ability to implement at this time. There is no reason to believe a proof-of-stake model is what is intended. Even the whitepaper states:

> The challenge is that as of today we do not believe that there is a proven solution that can deliver the scale, stability, and security needed to support billions of people and transactions across the globe through a permissionless network.

> Libra HotStuff BFT is not capable of achieving the throughput necessary for a payment rail

This seems like some actual benchmarks that simulate real system load are needed before a conclusion can be made.

> Libra’s Move language is unsound

It seems like the OP takes a more traditional view of type checkers as a Haskeller programmer. Pushing type-checking to the bytecode level is a very nontraditional approach to compiler design and contradicts the original Libra whitepaper claiming to implement linear types. Libra does not do this provide any linear typechecker or formal verification at this time.

> Libra’s cryptography engineering is unsound

This section is subject to some debate. It seems there are some unpublished audits of the libraries that may lend credibility to the Rust libraries but are unpublished. The original post doesn't claim that they are insecure, just that the more audits and testing the libraries undergo the more trusted they should become trusted (i.e. libsodium).

It also seems that Libra implements a lot of extraneous next-gen crypto that is dead code and not used for any purpose in the core logic.

> Libra has no capacity for consumer protection mechanisms

The section agrees with the OP that this does not exist.

Like most things, the kernel of tomorrow's ideas is already here. On the scale of the next five years, these ideas will give rise to what the future of programming will look like:

* Refinement types

Liquid Haskell: https://ucsd-progsys.github.io/liquidhaskell-tutorial/02-log...

* SMT Solver Language Integration

Cryptol: https://github.com/GaloisInc/cryptol

* Session Types

Scribble: http://www.scribble.org/

* Dependent Types

Agda: https://en.wikipedia.org/wiki/Agda_(programming_language)

Idris: http://www.idris-lang.org/

* Effect typing

Koka: https://research.microsoft.com/en-us/um/people/daan/madoko/d...

* Formal verification

Coq: https://www.cis.upenn.edu/~bcpierce/sf/current/index.html

TLA+: http://research.microsoft.com/en-us/um/people/lamport/tla/tl...

This is the general trend, generally making more composable abstractions and smarter compilers and languages that can reason about more of our programs for us.