[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.