When i was the focus of the rust community, and trending #1 on HN, i simply deleted my repos and disappeared.
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.
Absolutely!
The zz export command just dumps the C and SMT code along with makefiles for common build systems and stops there. Very handy for using it within other toolchains.
Prove of algorithms is possible as long as there's a known method of doing so in SMT. That means in practice, if someone has written a paper for formally proving an algorithm in SMT, you can mostly copy paste the proof.
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.
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.