Some people in that community reflexively see a conspiracy or invoke the CoC or use whatever other non technical tools they find to derail the discussion.

It's not even that they're always wrong or that I directly oppose the culture they want to have, but the shotgun blast of drama that this comes with is just so much effort to navigate that i decided to just never contribute to rust again.

Comments URL: https://news.ycombinator.com/item?id=24275158

Points: 4

# Comments: 0

That's partially because frankly i don't know yet. We'll have to discover slowly how far the first class proof expressions can be pushed.

the word "safe" here is actually gone now, because it indeed says something different. thanks for the feedback.

note that there are convenience tools to deal with heap-free targets (microcontrollers) such as tail variants (statically enforced flexible arrays):

https://github.com/aep/zz#metaprogramming-or-templates-tail-...

zz is developed in parallel with a large project using zz and new syntax sugar features will surface slowly as they become practically useful.

That being said, it will never replace external formal verification with something like coq. They serve a different purpose.

for example check out the err::checked() theory which enforces that a function call must be followed by err::check.

similarly, i expect a community will come up with other standard contracts such as must_not_copy() for secret values that may not be copied.