mm0
str0m
mm0 | str0m | |
---|---|---|
5 | 10 | |
293 | 244 | |
- | - | |
5.7 | 9.7 | |
about 1 month ago | 4 days ago | |
Rust | Rust | |
Creative Commons Zero v1.0 Universal | MIT License |
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.
mm0
-
Is Something Bugging You?
Along similar lines, Mario Carneiro wrote a formalisation of a subset of x86 in MetaMath Zero (https://github.com/digama0/mm0/blob/master/examples/x86.mm0) with the ultimate goal of proving that the MetaMath Zero verifier itself is sound. https://arxiv.org/pdf/1910.10703.pdf
(And of course Permutation City is a fiction book all about emulating computers with sound properties!)
- reconnecting with the math world after retirement
-
Is it possible to make concrete progress on the alignment problem using an abstract theory of formal control of computer systems? Any help or advice would be really appreciated.
For the first part I have no idea but for the second part I feel like one workable approach is formal control of computer systems. For instance we have a lot of formal mathematical systems (metamath, lean, coq, isabelle etc) and there are attempts to model computer architectures in these systems (there's a cambridge group working on a formalised version of the ARM architecture, and I know Mario Carneiro is working on MM0 which I think has formalised x86) which is all cool.
-
Category theory is a universal modeling language
Perhaps look into Metamath Zero / mm0 which.. well I'll just quote from the project [1]:
> Metamath Zero is a language for writing specifications and proofs. Its emphasis is on balancing simplicity of verification and human readability of the specification. That is, it should be easy to see what exactly is the meaning of a proven theorem, but at the same time the language is as pared down as possible to minimize the number of complications in potential verifiers.
> The goal of this project is to build a formally verified (in MM0) verifier for MM0, down to the hardware, to build a strong trust base on which to build verifiers.
[1]: https://github.com/digama0/mm0
-
The State of State Machines
IMO an interesting project in this space is: mm0 / MetaMath Zero - Closing the loop in proof verification down to verifying the machine code of the verifier. Goes from first-order logic to peano arithmetic to a model of x86 to a model of the verifier written in x86. Interestingly, it demonstrates that verification of a compact proof can be performed in linear time (!) if the proof is structured correctly. -- https://github.com/digama0/mm0
The fact that proof checking can take linear time (though not proof-finding), and the fact that it incorporates so many 'layers' has emboldened my opinion that such a thing as I described above is possible and has a enormous potential.
str0m
- VoRS: Vo(IP) Simple Alternative to Mumble
-
Interview with Mo Rajabi, co-founder and CEO of Noor
In the video, Mo talked about a few packages like Cidre and StrOm, and we referred to SpaceDrive.
-
Is Something Bugging You?
- Dropbox [3] uses a similar approach but they talk about it a bit more abstractly.
Sans-IO is more documented in Python [4], but str0m [5] and quinn-proto [6] are the best examples in Rust I’m aware of. Note that sans-IO is orthogonal to deterministic test frameworks, but it composes well with them.
With the disclaimer that my opinions are mine and mine alone, and don’t reflect the company I work at —— I do work at a rust shop that has utilized these techniques on some projects.
TigerBeetle is an amazing example and I’ve looked at it before! They are really the best example of this approach outside of FoundationDB I think.
[0]: https://risingwave.com/blog/deterministic-simulation-a-new-e...
[1]: https://risingwave.com/blog/applying-deterministic-simulatio...
[2]: https://dropbox.tech/infrastructure/-testing-our-new-sync-en...
[3]: https://github.com/spacejam/sled
[4]: https://fractalideas.com/blog/sans-io-when-rubber-meets-road...
[5]: https://github.com/algesten/str0m
[6]: https://docs.rs/quinn-proto/0.10.6/quinn_proto/struct.Connec...
-
Pure C WebRTC
I am really excited about https://github.com/sepfy/libpeer. It has examples ready for ESP32 etc....
When working on KVS I wasn't familiar with the embedded space at all. I saw 'heavyweight' embedded where you were running on Linux. Then you had RTOS/No OS at all. I wasn't prepared for these devices at all. If we can make WebRTC work in the embedded space I think it will really accelerate what developers are able to build!
Remotely driven cars, security cameras, robots in hospitals that bring iPads to infectious patients etc... Creative people are building amazing things. The WebRTC/video space needs to work harder and support them :)
-----
I love how diverse the WebRTC space is now. Outside of this implementation you have plenty of other options!
* https://github.com/shinyoshiaki/werift-webrtc (Typescript)
* https://github.com/pion/webrtc (Golang)
* https://github.com/webrtc-rs/webrtc (Rust)
* https://github.com/algesten/str0m (Rust)
* hhttps://github.com/sepfy/libpeer (C/Embedded)
* https://webrtc.googlesource.com/src/ (C++)
* https://github.com/sipsorcery-org/sipsorcery (C#)
* https://github.com/paullouisageneau/libdatachannel (C++)
* https://github.com/elixir-webrtc (Elixir)
* https://github.com/aiortc/aiortc (Python)
* GStreamer’s webrtcbin (C)
See https://github.com/sipsorcery/webrtc-echoes for examples of some running against each other.
- WebRTC for the Curious
- Show HN: Bring phone calls into the browser (sip-to-WebRTC)
- WebRTC support being added to FFmpeg
-
str0m 0.1.0 – Sans-IO WebRTC library
Find it here: crates.io/crates/str0m Code here: github.com/algesten/str0m Docs here: docs.rs/str0m/0.1.0/str0m/
-
str0m a sans I/O WebRTC library
Git: https://github.com/algesten/str0m
What are some alternatives?
ffmpeg - FFmpeg Zig package
broadcast-box - A broadcast, in a box.
go2rtc - Ultimate camera streaming application with support RTSP, RTMP, HTTP-FLV, WebRTC, MSE, HLS, MP4, MJPEG, HomeKit, FFmpeg, etc.
webrtc-echoes - Simple useful interoperability tests for WebRTC libraries. If you are a WebRTC library developer we'd love to include you!
webrtc - A pure Rust implementation of WebRTC
ffmpeg-webrtc - Support WebRTC(WHIP) for FFmpeg.
libpeer - WebRTC Library for IoT/Embedded Device using C
quinn - Async-friendly QUIC implementation in Rust
Pion WebRTC - Pure Go implementation of the WebRTC API
SIPSorcery - A WebRTC, SIP and VoIP library for C# and .NET. Designed for real-time communications apps.
libdatachannel - C/C++ WebRTC network library featuring Data Channels, Media Transport, and WebSockets
webrtc-for-the-curious - WebRTC for the Curious: Go beyond the APIs