Our great sponsors
- Onboard AI - Learn any GitHub repo in 59 seconds
- InfluxDB - Collect and Analyze Billions of Data Points in Real Time
- SaaSHub - Software Alternatives and Reviews
-
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...
-
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...
-
Onboard AI
Learn any GitHub repo in 59 seconds. Onboard AI learns any GitHub repo in minutes and lets you chat with it to locate functionality, understand different parts, and generate new code. Use it for free at www.getonboard.dev.
