That's unfortunate, I really preferred Whisky to crossover purely for the UX, I would happily pay for a crossover license if i got to keep the whisky app itself, crossover's ui is archaic and ugly in comparison.

basically every european country? they've all had much larger datacaps than north america for years preceding 5g and most are quite densely inhabited.

Sure, scopes are not as easily syntactically visible, but each assignment is creating a new scope, that doesn't change anything for equational reasoning which has to account for captures / substitutions anyways.

What do you mean? let-bindings don't interfere with referential transparency. `let x = 1 in let x = 2 in foo` is referentially transparent.

> * "As provable as Ada/SPARK": I'll let you read the design in [2] and decide for yourself. But Yao will also have contracts.

Without being too self-indulgent, I'm not sure there is that big of a gap between the two in provability, there are now a huge array of verifiers for Rust code which are being used to verify real code: SAT/SMT solvers, kernels, memory allocators etc...