BitCraft Online will be open source (the backend is written in Rust)
https://bitcraftonline.com/blog/open-sourcing-bitcraft-online
Discussions: https://discu.eu/q/https://bitcraftonline.com/blog/open-sourcing-bitcraft-online
linkspam!
15,000 lines of verified cryptography now in Python.
http://jonathan.protzenko.fr/2025/04/18/python.html
saved 2025-04-19 https://dotat.at/:/SO9A7.html
I have been waiting for this book for 28 years (see the first version of https://third-bit.com/ideas/not-on-the-shelves/) - thank you @TartanLlama
Does anyone have any good resources around automata and how to model systems with them?
I've seen the cellular automata demos, and they're fun! I've also used / written finite state machine implementations, and I tend to model a lot of things with them.
But I know that automata can go a lot further than that. For example, I know that the peep magic peephole optimizer is/was based on automata, and it's what made it efficient. I want to learn more about automata like that?
Help us create a vision for Rust's future, by taking part in our vision survey!
Check out the blog post: https://blog.rust-lang.org/2025/04/04/vision-doc-survey.html
@MartinEscardo
I had a question about univalent mathematics and I was told you'd be the one to ask. I hope you don't mind
Reading the HoTT book I noticed that they defined universes to be cumulative. This surprised me because in theorem provers such as Lean and allegedly Agda (I was told), this is not the case. In the book itself they mention a downside of having cumulative universes being that a term no longer has a unique type, but they don't mention any advantages of constructing them this way.
Therefore, my question is: what is the advantage of having cumulative type universes?
** Speaker announcement ** Catch this talk at RustWeek 2025!
Speakers: David Barsky & Lukas Wirth
Title: Salsa in Rust-Analyzer
Info & tickets: https://rustweek.org/talks/salsa/
See you in Utrecht 13-17 May, 2025!
When Signal was designed, our threat model was protecting the communications of civil society, journalists, just regular citizens ...
The threat model of military operations & sharing your hate of Europeans was not what Signal was designed for. Ephemeral messages and cryptographic deniability are not fit for communications that require accountability.
But I appreciate their effort to make government more efficient by adding journalists to the chat instead of requiring to go through FOIA.
I've now published my blog post, "I want a good parallel computer." https://raphlinus.github.io/gpu/2025/03/21/good-parallel-computer.html . Thanks much to all the feedback on the draft, I'd like to think I've clarified some things that might have been confusing.
There are just a few days left now to register for the Midlands Graduate School (MGS) in Sheffield, 7-11 April 2025. Eight fantastic courses on category theory, type theory, coalgebra, semantics and more.
Registration closes on Monday 24th March.
The first production ready version of The Rocq Prover 9.0 has been released today, see https://rocq-prover.org/releases/9.0.0 on our new official website! In the coming weeks, we'll migrate the Discourse, Zulip and Github organizations, please bear with us and don't hesitate to report broken links! Packages for opam and nix will be coming soon.
Computer Science and Mathematics