[ef4]

I'm excited for the ideas here and have been following Stellar.

But I'm hugely disappointed to see that they went with C and C++ for their new core codebase. This is the kind of code that needs strong safety, security, and correctness guarantees, and here in 2015 we have several mature languages with better safety & correctness guarantees.

C# and Java are both mature and mainstream, and either would have been a sane choice. Go is slightly less mature but also a safe and conservative choice.

(I personally love where Rust is going too, but I could excuse people for not choosing it yet due to immaturit.)

[VienneseCPA]

When your software aspires to move billions of dollars of value, it would ideally be written in Ada.

That said, I agree that C# and Java are good options.

What's hilarious is all of the Bitcoin startups that are running on node.js and mongodb. Would you put your kids on a flight if you knew the control system was written with javascript and mongodb? Yikes.

[rational-future]

You are partially right. It is completely possible to write in JS/Mongo systems as robust as Ada/Oracle|DB2|SQL Server. You just have to know what you are doing. There is no magic in Ada, Oracle, etc.

Node and Mongo are moving hundreds of billions daily in HFS shops.

[SkyMarshal]

>There is no magic in Ada, Oracle, etc.

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.

[lectrick]

Actually, having met a few of them, a surprising number are using PHP, which made me quite angry lol.

[flatline]

C/C++ are going to be tied to some runtime libraries but that doesn't seem like as big an externality as being tied to a particular version of an entire VM. You may prevent certain classes of of programming error with a memory-managed language but at the cost of fine-grained control of your memory, and when it comes to security software in general and key management in particular you expose yourself to a whole other set of issues with managed memory. C/C++ are also highly portable, arguably moreso than Java (and certainly moreso than C#). They seem like the safest choice in many ways.

[ef4]

FWIW, Go has no VM, and neither does Rust. They compile real binaries.

And Rust gives you fine-grained memory control without sacrificing safety -- unlike the others it has no garbage collector, and instead proves allocation safety at compile time. In Rust you can know for sure exactly where your key has been copied and when it will get deallocated (to the extent that any program running in virtual memory on normal hardware can know that).

Although I agree that these are the less mature choices, and it's reasonable to reject them for that reason.

[tlrobinson]

Meh, Bitcoin seems to be doing ok with C++.

It's certainly had a few issues, though I haven't looked closely enough to know which are due to the lack of memory safety, etc: https://en.bitcoin.it/wiki/Common_Vulnerabilities_and_Exposu...

[jude-]

If a program is formally proven to be correct, it doesn't matter what language it's written in.

[ef4]

Agreed, but that's not what they did here. They didn't prove the program is correct, they proved the algorithm is correct. It remains to be seen how closely the program actually implements the algorithm in the paper.

[jroesch]

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.

[jude-]

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

[rational-future]

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

[ryanobjc]

I'm not sure I'd call Java for systems programming is a "sane" choice, but ok!

I think with a very modern C++ approach and very careful coding you can rock out. Yeah not everyone has this, but the losses from using Java is just so huge!

[dward]

A consensus algorithm targeted for use in a globally distributed OLTP is hardly "systems programming".

[ryanobjc]

Shovel data around at speeds that push the boundaries of hardware performance. That isn't systems programming?

[rational-future]

Well it's first and foremost a protocol. Feel officially invited to implement it in any language you like. Language correctness guaranties sounds to me as a term from MBA programs and business magazines and not something a REAL dev would EVER say.

I've been to at least 200 software conferences in my life and never heard speakers like Linus, Ken Thomson, RMS, Gordon Letwin, DHH, Anders Hejlsberg mention "correctness guarantees".

[ef4]

"Correctness guarantees" is a whole bucket of things you certainly have heard of, like: bounds checking, integer overflow protection, or statically safe memory allocation.

I'm not talking about a whole-program correctness proof -- although those do exist too.