Example: seL4 is written in C (as in, written by hand by fallible humans--not compiled down from a higher-level language [1]). But, the C is written in such a way that it is feasible to prove its equivalence to a Haskell prototype which had previously been proven correct.

Yes, language choice can be important. But, the degree of its importance depends on what you're building with it and how you're using it.

[1] http://www.nicta.com.au/pub-download/full/7371

He is even credited in the changelog: http://lwn.net/Articles/131744/

[0] https://www.reddit.com/r/programming/comments/31yi7d/graydon...

[1] https://lkml.org/lkml/2005/4/6/121

There is no magic but there are strong constraints that shift reliance for correctness from fallible human programmers and peripheral tools to the type system and compiler, providing better integrated, systematic assurance.

There's one sense in which FBA is stronger than the Internet analogy, however, it that is is actually testing transitive reachability. So instead of just making sure you can talk to those 50 web sites, you actually make sure all of those 50 web sites can talk to all the sites they consider important, and so on, until you get the transitive closure, which is basically the notion of an FBA quorum.

Part of the goal of SCP is to leave such policy questions up to the market and see what kind of architecture emerges. Our hope is that this flexibility combined with the lower barrier to entry will lead to greater financial inclusion as people build on our platform. But if we add too many policy restrictions, we risk heading off unanticipated innovations. (Heck, someone might literally replicate the Bitcoin policy and configure their quorum slices to trust 67% of whoever mined a Bitcoin block in the past week. That wouldn't really make sense, but it's possible.)

That said, what you're getting at is that with flexibility comes risk. We can't a priori rule out the possibility that organizations will choose bad quorum slices that violate safety. But we need to ask under what circumstances people care about safety and why. People obviously won't care about forks if one of the branches is purely a Sybil attack. But they likely will care if "real organizations" diverge, for some notion of that term. The reason, again, is that at some point the "real organizations" will affect one another in the network, however indirectly--maybe after a chain of five payments. That kind of indirect link is precisely what FBA quorums capture in the transitive closure of slices. So if everyone depends on the financial institutions they expect to do business with, and the whole economy is in fact interconnected, then Stellar will be safe.

I obviously believe such interdependence exists, and fully expect Stellar to be safe, but I can't predict exactly what the network will look like. Nor do I want to, as this could limit innovation. Only time will tell how this plays out.

I can't predict the future, but I do think it is likely that a bunch of de facto important players will emerge and have fairly complete pairwise dependencies. One reason is that Stellar follows a gateway model, where counterparties issue credits. So for example, down the line people might want to store their money as Chase or Citibank USD credits. So people will already have some notion that some participants are trustworthy enough to hold their USD deposits, and these institutions will emerge as important. If I'm a Citibank customer and you send me money, I obviously won't consider the payment complete until Citibank says it is. And of course Citibank is likely to want to depend on a bunch of institutions they do business with, so even just one bank should give me good transitive reachability.

But the nice thing about safety is that you can reduce any individual party's trust by depending on more people. So for example Stellar will run a validator node for the foreseeable future, and their incentives are different from Citibank's. To gain more trust in the system, I might want to wait for both Stellar and Citibank to agree before considering any payment fully settled.

Now, regular nodes add the non profit node to each of their 2 member set slices. If one of the bigger guys colludes, the system is only blocked, because now the regular stellar users have depended on the non-profit node in each stellar slice, who has seen the collusion and isn't externalizing bogus transactions. Once the collusion is published by the whistle blower node, regular stellar nodes can remove those slices that contained the bad node, and the system moves forward.

Now this is a completely contrived example but you can generalize it as a chain of trust webs, where i listen to the someone, someone listens to me and the person i listen to, and so on.

The primary reason why that does not apply here is because nobody is selling "the market at large" to you as a cryptographically-secure decentralized consensus system. And besides, those ledgers are edited all the time by Authorities; it's irrelevant to this topic.

Edit: you are attempting to reason by analogy about a pricing system, and then trying to apply it to proof-of-work consensus? May I ask why?

But they're not keeping consensus ledgers for limited supply cryptocurrencies. Any of these failures or faults can allow a coin to be spent twice (or other mutually excluded transaction) with parties that have different views of the system, the result-- and any transaction which is casually depended on the conflict-- can never be part of a common system.

So it's like someone manipulates the market economy to convince you to buy a cheeseburger most other parties think they sold to someone else, and now your hand cannot interact with your neighbor's door because your hand contains atoms that-- as far as your neighbor's door is concerned-- aren't part of your hand but are instead part of my foot.

Markets are a tool. They have their applications and limitations, building the security of a cryptocurrency in an adversarial environment out of them sounds like a plan for failure. No less than using a cryptosystem in a place where you really needed a market may not give great results.

But you don't have to take my word for it, the prior consensus model in Stellar _already_ faulted, all on its own when, the requirement for the trust topology was violated. This fault wasn't a surprise, I (and others) called it out years before-- but the vulnerability of the system was publicly ignored by Stellar's creators while they ran Ripple and Stellar's advisers (including Mazieres, who was an adviser listed on the Stellar site on day one) even as they facilitated the sale of their ripple-reboot asset to the general public. It was not acknowledged until it knocked their system out. The improved consensus may better confines the failure domain, but retains the property that the safety of the consensus is largely external and depends on particular topological constraints without a procedure that provides any assurance the constraints are likely to be met.

Another response to me argues that it will probably be fine; but this flys in the face of reason. The same property existed before and it demonstratively wasn't fine.

If you look at the old BCT thread, I was a big fan of the original ripple IOU system, before ripple labs bought the name, and had recommended it as a potentially fruitful area to many people. The original system could potentially have been implemented without any global consensus at all, which was a large part of why I found it interesting-- Global consensus is enormously costly. But functionality like a new cryptocurrency currency for the purpose of funding the company and the integrated non-interactive rippling (which apparently has been largely turned off in ripple now due to other security vulnerabilities) brought back in the global consensus requirement. (The result was that I felt I had to go edit all my old posts to remove my recommendations, since the system was wildly changed to be something else)

That's the Maginot Line attack, at Tim Swanson calls it. The more realistic attack is that China just hacks into five data centers and serves a warrant to another ten. An interesting property of the PoW incentive structure is that there is actually fairly little incentive to protect oneself against hacks, so I would not be surprised if it was fairly easy.

> By hacking enough organizations to take control of their nodes?

The key point in Stellar consensus is that even if enough nodes are hacked, then users can just stop trusting them and switch to other nodes, and so the network would "route around" the damage. With Bitcoin PoW, there's no way to exclude an attacker from participating; you have to accept their work just as much as everyone else's.

Because the prior version _already_ faulted in production as a result of having a trust graph that didn't meet the prior criteria needed for safety. The prior version also resulted in centralization in practice (in it's ripple instantiation; kind of neat that the ripple->str-reboot let us see both of the predicted failure modes play out, even though they were largely mutually exclusive)

The latest work is intended to relax the requirements/consequences but still provides no guidance or tools for achieving the required topology in practice.

By all means, clearly label these efforts that have have taking a "you haven't yet proved its broken" approach to safety/security; and I won't complain about them. Absent that, I just normally expect that when someone produces a cryptographic product that they've actually given some care to their security.

> consequence is that people will start putting the Stellar equivalent of blockchain.info onto their trust list in order

Then if they're anything like the Bitcoin world's blockchain.info-- which is regularly in a confused state--, I'm may soon find myself the proud owner of infinity STR, I guess? ( Screenshot someone else sent me of the actual BC.i site one day a while back: http://people.xiph.org/~greg/21mbtc.png )

"testing is making sure it does what it should, security auditing is making sure that is all it does"