Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality. Learn more →
Mm0 Alternatives
Similar projects and alternatives to mm0
-
Zulip
Zulip server and web application. Open-source team chat that helps teams stay productive and focused.
-
-
InfluxDB
Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
-
-
-
hermit
Hermit launches linux x86_64 programs in a special, hermetically isolated sandbox to control their execution. Hermit translates normal, nondeterministic behavior, into deterministic, repeatable behavior. This can be used for various applications, including replay-debugging, reproducible artifacts, chaos mode concurrency testing and bug analysis. (by facebookexperimental)
-
SaaSHub
SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives
-
-
-
NOTE:
The number of mentions on this list indicates mentions on common posts plus user suggested alternatives.
Hence, a higher number means a better mm0 alternative or higher similarity.
mm0 reviews and mentions
Posts with mentions or reviews of mm0.
We have used some of these posts to build our list of alternatives
and similar projects. The last one was on 2024-02-13.
-
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.
-
A note from our sponsor - InfluxDB
www.influxdata.com | 1 May 2024
Stats
Basic mm0 repo stats
5
288
5.7
about 1 month ago
digama0/mm0 is an open source project licensed under Creative Commons Zero v1.0 Universal which is not an OSI approved license.
The primary programming language of mm0 is Rust.
Sponsored
SaaSHub - Software Alternatives and Reviews
SaaSHub helps you find the best software and product alternatives
www.saashub.com