"An accessible syntax that makes it less scary."

Can anyone explain how syntax elements such as { } are a net win? This looks like they've tuned the syntax to not scare anyone off in the first week, at the expense of an economy of expression later.

Rob Pike once justified C syntax for its ability to survive pipes that mangled whitespace. That was then, this is now. To this old C programmer, anything that unnecessarily resembles C is ground glass in the eye.

I don't know, for me this doesn't look enough like C (or anything familiar).

I would love a language like C# or Python where you could just put in preconditions using the expression syntax of the language, and it would try to prove it. If it can't prove it, it might ask for more facts, give a warning, or add a runtime assertion. As far as I know the only language that does this was the experimental Spec#.

I would even go further and have complex preconditions as part of the types, so you could have say a Person with field "age" < 18 is of type Minor. (I know this is tricky. The objects would be immutable, or you'd only be able to specify Person|Minor and only narrow it with an assertion, for example). Nim has something a little bit in this direction with distinct types, and integer range types.

That's exactly what Ada2012 and SPARK2014 did. You write your contracts (preconditions, postconditions, assertions, contract-cases, invariants, type predicates) in Ada syntax and you get both runtime assertions and proof depending on which tool you call (compiler or prover). You give more facts when proof fails. You can tag code as 'ghost' and it's only available for proof tools...

To be able to be a bit more 'terse' in assertions, they added quantifiers, expression functions, case- and if-expressions. Lots of small improvements to allow contracts, that are finally a boon to write simpler and clearer code.

Everything you're asking for here is available in Ada2012 and SPARK2014.

here is an example using mirai and contracts:

https://github.com/facebookexperimental/MIRAI/blob/master/ex...

(note: the contracts crate can be used for verifying at runtime as well)