Our great sponsors

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...

rustzerocostabstractions
Testing out a Zero Cost Abstraction in Rust compared to similar approaches in C# and Java
Your "runtime" 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/mikebarber/rustzerocostabstractions
* https://carette.xyz/posts/zero_cost_abstraction/
* https://ruudvanasseldonk.com/2016/11/30/zerocostabstractio...

InfluxDB
Build timeseriesbased applications quickly and at scale.. InfluxDB is the Time Series Data Platform where developers build realtime applications for analytics, IoT and cloudnative services in less time with less code.