electrolysis
winnow
| electrolysis | winnow | |
|---|---|---|
| 2 | 8 | |
| 322 | 397 | |
| - | 8.6% | |
| 10.0 | 9.6 | |
| about 7 years ago | 20 days ago | |
| Lean | Rust | |
| GNU General Public License v3.0 or later | GNU General Public License v3.0 or later |
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
electrolysis
-
What Vale Taught Me About Linear Types, Borrowing, and Memory Safety
How do you represent this?
However, this insight holds for relatively common forms of ownership, and you can see this exploited in electrolysis: https://github.com/Kha/electrolysis
-
Magma, a project I hope will make provably correct software possible for everyone
In my opinion the best way of going about it is translating the Rust to Coq that has the same semantics (but different performance) as pioneered in https://github.com/Kha/electrolysis. Unfortunately that project isn't usable today as it requires an ancient version of Rust and Lean.
winnow
-
nom > regex
I truly love Nom, it made parsing really fun. I suggest trying out https://docs.rs/winnow which is a fork of Nom with a lot of nice features, I find it much more usable.
-
What Vale Taught Me About Linear Types, Borrowing, and Memory Safety
I feel like I'll have to read up some more to have the background to fully understand the article but one thing I wanted to point out is a difference between `fn rand_int(rand: &mut Random) -> i64` and `fn rand_int(ran: Random) -> (i64, Random)`, at least in Rust. With the version that moves `Random`, the return type is bigger and may spill over from registers to the stack which may cause a significant slow down, more than the code of Vale's generation check, I suspect.
I've run into this with my parser combinator library, winnow [0], and am considering switching from the nicer functional model of moving to the more imperative model of `&mut` [1].
[0]: https://docs.rs/winnow/latest/winnow/
[1]: https://github.com/winnow-rs/winnow/issues/72
-
`nom-derive` Derive parser from structure definition
Done. For people that want to follow this, here is the link.
-
easy way to produce a parser
winnow, fork of nom
-
winnow = toml_edit + combine + nom
What are your thoughts on https://github.com/winnow-rs/winnow/pull/199 ?
What are some alternatives?
Rudra - Rust Memory Safety & Undefined Behavior Detection
nom - Rust parser combinator framework
line-combination-proofs
chumsky - Write expressive, high-performance parsers with ease.
fiat - Mostly Automated Synthesis of Correct-by-Construction Programs
pest - The Elegant Parser
magmide - A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
prusti-dev - A static verifier for Rust, based on the Viper verification infrastructure.
tectonic - A modernized, complete, self-contained TeX/LaTeX engine, powered by XeTeX and TeXLive.
rust-verification-tools - RVT is a collection of tools/libraries to support both static and dynamic verification of Rust programs.