a3p

4 ms·

1.
by a3p 2y ago
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
2.
Mad hax (tm) packing JSON smaller than msgpack, protobuf, gzip and even zstd(github.com)
4 points by a3p 6y ago|0 comments
3.
by a3p 7y ago
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.
4.
by a3p 7y ago
Author here. fully agree that the description is vague and doesn't really tell you where it stands versus something like F* , SPARK, etc. That's partially because frankly i don't know yet. We'll have to discover slowly h
5.
by a3p 7y ago
it is https://devguard.io/ which is being rewritten from rust to ZZ in this branch https://github.com/devguardio/carrier/tree/zz
6.
by a3p 7y ago
the standard library does not allocate any heap memory, but heap modelling will be added to the prover eventually. note that there are convenience tools to deal with heap-free targets (microcontrollers) such as tail variants (statically enf
7.
by a3p 7y ago
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
8.
by a3p 7y ago
that is correct. however, zz does enforce api contracts which can be arbitrary expressions within the QF_UFVB theory. for example check out the err::checked() theory which enforces that a function call must be followed by err::check. simila