Stellar Consensus Protocol: Proof and Code

He also did a little write-up around this stuff:

http://graydon2.dreamwidth.org/201698.html

I guess you missed the /s at the end. As the perfect program runs on top of buggy hardware, OS, libraries, VMs, etc.

Language choice can be important. If you do the common thing and build a distinct model of your program and prove it correct your guarantees don't hold about the actual implementation. You need a second method to ensure equivalence between your model and implementation, this obviously requires much more work and can vary greatly based on the tools and programming languages involved.

Yes--choose the language and development process that makes it easiest to reason about the desired properties of the program.

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

Walter from Kraken here - I really enjoyed this thread!

(Bit sleep-deprived right now but) FWIW, here's my take: Bitcoin tries to be too many things to too many people. Original ripple was a great response, though without providing a strong solution to the topology problem (manual processes for trust agility).

Now, both fail to "do one thing and do it well". Fundamentally, the functions 'settlement protocol', 'currency' and 'client program' (ie. implementation of protocol) should be well delimited. Besides these, Bitcoin now effectively attempts to do more (expensive paid public sequential datastore and agent-based computing platform, ill-conceived invoicing system, future revenue-guarantees for early adopters/special nodes, etc.)

This brings me to some points I feel have not been considered in this thread: (1) People don't put absolute trust in a settlement network or currency. The de-facto means of managing risk is to simply to limit exposure: either by sending smaller amounts sequentially over time and validating delivery with your endpoint (out of band) prior to sending the next 'chunk'; or by splitting a transaction across multiple currencies/settlement networks/(anonymous/temporary/unpredictable) points of network connectivity. (2) No system fits all people. It's great that the stellar notion addresses one of Bitcoin's most glaring issues: latency for real time / retail transactions. However, it does not necessarily meet all of Bitcoin's capabilities, nor should it aim to. A real world user should have a computationally available means of comparing these networks against real time requirements to select an appropriate path (in terms of risk mitigation strategy, temporal requirements, maximum transaction size limitations, secrecy requirements, and any other execution and routing goals/preferences). (3/corollary) The key issue in present-era financial systems may be that business logic around the true properties of a financial transaction, network or settlement partner are very rarely formally defined (ie. typically many pages of indecipherable legalese that amount to 'we promise nothing and have well paid lawyers', with no computationally usable community metric for SLA enforcement on latency, reliability, instances of failure, etc.)

My thoughts here have remained fairly constant for the last four years: what is really needed is a business-level transaction protocol that disclaims any affinity at all for (a) the currency or currencies in a transaction; (b) the settlement systems used; (c) the endpoint identification system used; (d) allows the discussion/agreement of a realistic range of resolution strategies for common problems in business-level transactions; and (e) facilitates flexible (indeed, multi-path) routing between endpoints across arbitrary financial service providers, potentially using multi-hop/multi-asset pathways shortlisted in real-time through actor and transaction-specific requirements.

A valid settlement path should be 'buy expensive art, get on a plane, deliver to mansion'. Likewise, a valid settlement path should be 'plant a tree and share the GPS location and have it manually validated by a third party'. (These are outlying examples, but an example of the degree of flexibility that should be aimed for in the long tail of latency and use cases. The shorter side is obvious: redundant multi-provider fiscal routing (even across conventional banks), level playing field for emergent financial systems and the conventional ones, etc.)

Some time ago I tried to make proposals in this area at http://ifex-project.org/ (IIBAN perhaps most successfully) but have not been able to dedicate much time to the notion lately. I do however feel it is relevant and am willing to jump at any time to work with others to move the notion forward. If you two are interested I'd love to get together and bash something formal and extensible out of this line of thinking. Tentative proposal: meeting in Europe next month?