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.

Anthony Cowley has given some really amazing Haskell talks in the past, this keynote should be amazing.

http://vimeo.com/m/77164337

Static typing is mostly orthogonal, Haskell is mostly blazing fast because of all the aggressive compiler optimizations and the last decade of hard work by Simon Marlow and others on the parallel runtime.

In my experience the failure rate is far below 5% for vanilla HM algorithm. I've never seem a pathological input in the wild that wasn't contrived specifically to test the typechecker.

I'm glad that you've taken the time to write more. Your posts have been very articulately stated, especially the one on type systems.

Please don't do this. We have enough problems communicating this concept as it is.

It's not a pedantic distinction given how much the term has been overloaded to refer to dissimilar concepts.

I think this really gets to the core strength of Haskell, which for me has always been having code that we can rapidly prototype but migrate into production and have living in the codebase for a long time. I've written code in good deal of languages and haven't found a language with the power/weight ratio that Haskell has.

The slight cost I have found though is that a lot of the tools he mentioned have a rather steep learning curve ( monads, parsec, repa, conduits, lens ) especially for those coming from an imperative background. But learning any of them is an investment in your programming skills that pays off ten-fold down the road.

Lots of great Haskell material on his site. In particular this derivation of the State monad from first principles was the "Aha!" moment for me understanding monads.

http://dev.stephendiehl.com/begin/index.html#monads

This is a post about categorical monads, I assume this is why it doesn't use the standard symbols that the Haskell monad uses (>>=, return) and instead refers to the natural transformations (η, μ) as mathematicians do.

[1] http://ncatlab.org/nlab/show/monad#definition_18