-
It's always a pleasant surprise to see people using Coq and other formal verification technology. We need more rigor in programming! If this article gave you a thirst for interactive theorem proving and you want to learn it from the ground up, I've recently written a Coq tutorial [1] which covers topics like programming with dependent types, writing proofs as data, and extracting verified code. That repository also contains a handy tactic called `eMagic` [1] (a variant of another useful tactic called `magic` which solve goals with existentials) which can automatically prove the theorem from the article.
[1] https://github.com/stepchowfun/proofs/tree/main/proofs/Tutor...
[2] https://github.com/stepchowfun/proofs/blob/56438c9752c414560...
-
InfluxDB
InfluxDB – Built for High-Performance Time Series Workloads. InfluxDB 3 OSS is now GA. Transform, enrich, and act on time series data directly in the database. Automate critical tasks and eliminate the need to move data externally. Download now.
-
rust-zero-cost-abstractions
Testing out a Zero Cost Abstraction in Rust compared to similar approaches in C# and Java
Your "run-time" code with iterators vs with a hand made for loop tends to result in the same set of instructions. Often the iterator usage will also enable optimizations that make the loop faster.
* https://github.com/mike-barber/rust-zero-cost-abstractions
* https://carette.xyz/posts/zero_cost_abstraction/
* https://ruudvanasseldonk.com/2016/11/30/zero-cost-abstractio...
