| ▲ | amelius 9 hours ago |
| If the tutorial uses Rust, why didn't they use a solver written in Rust? Z3 was written in C++. |
|
| ▲ | invl 3 hours ago | parent | next [-] |
| I'm not sure I understand your argument. Z3's API is canonically C. There's a C++ wrapper that works pretty well. I don't have experience with the Rust wrapper, but I'd imagine that works pretty well too. |
|
| ▲ | 8 hours ago | parent | prev | next [-] |
| [deleted] |
|
| ▲ | suddenlybananas 9 hours ago | parent | prev [-] |
| What solver would you have them use? Z3 is very mature and the Rust bindings are pretty good in my (limited) experience. |
| |
| ▲ | amelius 9 hours ago | parent [-] | | I would write the tutorial in C++, for a more direct experience. | | |
| ▲ | Arainach 7 hours ago | parent | next [-] | | There's nothing "more direct" - the different APIs for different languages call into the same underlying library, and most of them are more accessible and easier to work with than C++. Z3 is presumably written in C++ for performance, but without data I am very confident the vast majority of programs that use Z3 consume it via one of the other APIs. | |
| ▲ | volemo 8 hours ago | parent | prev | next [-] | | I personally like to avoid the “writing in C++” experience. :/ | | |
| ▲ | amelius 8 hours ago | parent [-] | | The authors of a powerful solver package thought differently. | | |
| ▲ | onair4you 8 hours ago | parent | next [-] | | It might have more to do with the first release of Z3 being in 2012, with the first stable Rust release being in 2015. Rather than the authors of Z3 passing some kind of judgment on Rust… | | |
| ▲ | amelius 7 hours ago | parent [-] | | Z3 uses a sophisticated and fast garbage collection scheme internally that doesn't mesh well with Rust idioms. | | |
| |
| ▲ | mcphage 6 hours ago | parent | prev [-] | | The authors of a powerful solver package were solving a different problem than the users of a powerful solver package, and so different tools may be appropriate. |
|
| |
| ▲ | suddenlybananas 8 hours ago | parent | prev [-] | | The author might not know C++ and you don't need to use C++ to effectively use z3. |
|
|
