magmide
tectonic
Our great sponsors
magmide | tectonic | |
---|---|---|
22 | 22 | |
801 | 3,697 | |
1.0% | 2.1% | |
6.9 | 9.2 | |
20 days ago | 4 days ago | |
Coq | C | |
- | 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.
magmide
-
Languages on the rise like Rust and Go are being quite vocal against inheritance and many engineers seem to agree. Is this the end of inheritance? What do you think?
https://github.com/magmide/magmide when
-
Kani 0.29.0 has been released!
How close are we to this https://github.com/magmide/magmide
-
Make formal verification and provably correct software practical and mainstream
I really want to like this, but it really comes across as more of a wishful thinking project without a lot of experience or intuition about how to solve the very real problems that formal methods run into in this domain. Like, the design goals literally include "verify any program" [1], which is almost certainly impossible.
Important questions like how you implement the design pillars without running smack into the issue of decidability seem entirely ignored. They have a whole section on how "this idea exists in an incentive no man's land" without seemingly being aware of the rich history of formal methods in low level programming, from Ada through Java through formal C through Rust itself. The common issues these encountered like decidability, holes in the formal model (which contributed to the downfall of the Java sandbox as a security boundary), and the combinatorial explosion inherent in verification tools are all huge looming questions that should at least be mentioned.
Maybe I'm being overly critical here, but it all makes me wonder whether the project is even possible.
[1] https://github.com/magmide/magmide/blob/main/posts/design-of...
-
Hello Letlang! My programming language targeting Rust
I would love to play around with a compiled language with as powerful a compile-time type system/proof assistant as Lean or Coq. I saw some early work in the Rust realm here: https://github.com/magmide/magmide
- Software can literally be perfect (talks about some important logical ideas that make the Rust ownership system work, and how we could build a provably correct Rust compiler)
-
My Path to Magma
The Magma name requires disambiguation:
His Magma programming language: https://github.com/blainehansen/magma
> The goal of this project is to: create a programming language and surrounding education/tooling ecosystem capable of making formal verification and provably correct software mainstream and normal among working software engineers.
Magma computer algebra system: https://en.wikipedia.org/wiki/Magma_(computer_algebra_system...
> Magma is a computer algebra system designed to solve problems in algebra, number theory, geometry and combinatorics. It is named after the algebraic structure magma. It runs on Unix-like operating systems, as well as Windows.
-
Magma, a project I hope will make provably correct software possible for everyone
The current design thinking is spelled out in the repo: https://github.com/blainehansen/magma
The idea with notations isn't to make custom symbology impossible, just clearly signaled, much in the same way Rust macros can do whatever they want but have to be underneath some macro_name!esque indicator. Check out my rough design thoughts for more if you're interested :) https://github.com/blainehansen/magma/blob/main/posts/design-of-magma.md
tectonic
-
I rewrote my CV in Typst and I'll never look back
You may want to try https://github.com/tectonic-typesetting/tectonic, which downloads files from TeXLive on-demand.
-
bard 2.0
v2 has improved TeX engine lookup, improved PDF template look&feel, proper support for MS Windows (where it comes integrated with the Tectonic engine) and a few more new features.
-
[Media] Version 0.3 of Inlyne - An interactive markdown renderer written entirely in Rust
There's https://github.com/tectonic-typesetting/tectonic but I think the issue with that idea is that sure, you can re-implement TeX (it's sufficiently simple) in Rust and then run LaTeX packages on top of it, but then you're back to LaTeX and all its weirdness so you haven't really gained anything compared to LaTeX itself.
-
Another rewrite in rust: Pydantic
tectonic: https://github.com/tectonic-typesetting/tectonic
- \begin{mess}
-
UnTeX - Parsing and formatting TeX documents with Rust - Looking for help
How does it compare with Tectonic?
-
Brian Kernighan adds Unicode support to Awk (May, 2022)
> He says he wanted to try "XeTeX" (which supports Unicode) but "...I was going to download it as an experiment and they wanted 5 gigabytes and 5 gigabytes at the particular boonies place I'm living would...mmm..not be finished yet!"
He can try "Tectonic" [0] - a modern XeTeX based TeX/LaTeX distribution that installs a minimum system and then downloads and installs dependencies on-demand. Tectonic is written in C and Rust [1].
It's sad that Tectonic conversion to Rust[1] was never finished. For now it's just a wrapper around C and C++ code. By far, it was the most promising thing in this distribution.
[1] https://github.com/tectonic-typesetting/tectonic/issues/459
This has been done and yes people should switch to this. "Tectonic automatically downloads support files so you don’t have to install a full LaTeX system in order to start using it. If you start using a new LaTeX package, Tectonic just pulls down the files it needs and continues processing."
-
LaTex alternative/replacement written in Rust?
The only thing I've seen is https://github.com/tectonic-typesetting/tectonic but that's an actual re-implementation of TeX Rust.
What are some alternatives?
miktex - the MiKTeX source code
texlab - An implementation of the Language Server Protocol for LaTeX
tex-rs - A port of TeX82 to Rust. (WIP)
Oberon - Oberon parser, code model & browser, compiler and IDE with debugger
Rudra - Rust Memory Safety & Undefined Behavior Detection
arara
github-orgmode-tests - This is a test project where you can explore how github interprets Org-mode files
rpm-ostree - ⚛📦 Hybrid image/package system with atomic upgrades and package layering
mdbook-pdf - A backend for mdBook written in Rust for generating PDF based on headless chrome and Chrome DevTools Protocol. (用 Rust 编写的 mdBook 后端,基于headless chrome和Chrome开发工具协议生成PDF)
line-combination-proofs
prusti-dev - A static verifier for Rust, based on the Viper verification infrastructure.
tectonic - Experimental Oxidization of Tectonic the TeX/LaTeX engine.