The mathematics community's motivation for formalizing problems like Maryna Viazovska's sphere packing results in Lean weren't because the results were in doubt -- she won a Fields Medal for it, it's an extremely examined proof -- but because formalizing those results would lead to a lot of interesting and useful mathematical objects needing to be formalized as a prerequisite, which could then be merged into Lean's Mathlib and become useful for anyone working with Lean, particularly students. Having a library of idiomatic proofs available in a formal system capable of checking your work is Really Cool! Working in a proof assistant is a great way to develop mathematical maturity, especially for people who might not have an undergraduate education available to them.

(Unfortunately in the sphere packing case, the research group working on it made the mistake of trusting one of the various "AI for Math" slop companies, who promptly rugpulled them: https://arxiv.org/html/2603.03684v3)

So the short answer is "it depends on what you want". Lean is an eminently usable system for humans and LLMs alike; Metamath is uh. Not. But yes, Metamath seems to have a more trustable kernel wrt. the independent verifiers, so if that's all you're after it would be a better pick. But... there's only so many bugs Lean's kernel can have. At some point, they'll all be found.

(This actually interferes with Typst's math mode. But you can manually construct math blocks, so no real problem. Pandoc variables are only valid within templates anyway.)

https://pandoc.org/MANUAL.html#variables-set-automatically

I love Rust, but you couldn't pick a language with slower compile times... XD

I believe its adoption was motivated by needing to write/generate an OTF parser.

Their SpecTec system is fancy and neat but I don't think that auto-generated specifications produce something worth reading. Perhaps in the future when there's less churn, there might be a hand-written specification? In the mean time I've needed to jump into their Discord to ask clarification questions about the high-level stuff. Once understanding that and the grammar conventions and the like, the specification becomes much more readable, though still not great.

Certainly nothing like an RFC. But maybe I have too high standards...

There just aren't any open-source Android libraries for RCS out there, much less anything in AOSP.

https://github.com/search?q=rcs+android&type=repositories

https://lobste.rs/s/q8lz7a/what_s_condition_system_why_do_yo...

The difference comes in their use. There's two things of note. First, the implementation of an interface is static. It's known at compile time. For any given concrete type, there is at most one implementation of MovieApi. You're using the interface, then, to be generic over some number of concrete types, by way of only specifying what you need. Effect handlers aren't like this. Effect handlers can have many implementations, actually. This is useful in the case of ex. adding logging, or writing tests to simulate I/O without actually doing it, or just having different behavior at different places across the program / call stack...

    eff MovieApi {
      def getPopularMovies();
    }
    def main() {
      run {
        println("Alice's movies: ", getPopularMovies());
      } with handler MovieApi {
        def getPopularMovies() = [
          "Dr. Strangelove", 
          "Lawrence of Arabia",
          "The End of Evangelion",
          "I Saw the TV Glow"
        ];
      }
      run {
        println("Bob's movies: ", getPopularMovies());
      } with handler MovieApi {
        def getPopularMovies() = [
          "The Magic School Bus: Space Adventures",
          "Spy Kids 3-D: Game Over",
          "Twilight: Breaking Dawn: Part II"
        ];
      }
    }

So to answer your question more briefly, effects differ from interfaces by providing 1) a decoupling of implementation from use and 2) the ability to encompass non-local control flow. This makes them not really compete with interfaces/classes even though the syntax may look similar. You'd want them both, and most effectful languages have them both.

("The same" being a bit relative, here. Nim's sum types are quite a bit worse than those of an ML. Better than Go's, at least.)

So for ergonomics: reference counting is not a complete system. It's memory safe, but it can't handle reference cycles really very well -- since if two objects retain a reference to each other there'll always be a reference to the both of them and they'll never be freed, even if nothing else depends on them. The usual way to handle this is to ship a "cycle breaker" -- a mini-tracing collector -- alongside your reference counting system, which while is a little nondeterministic works very reasonably well.

But it's a little nondeterministic. Garbage collectors that trace references, and especially tracing systems with the fast heap ("nursery" or "minor heap") / slow heap ("major heap") generational distinction are really good. There's a reason tracing collectors are used among most languages -- ORC/ARC and similar systems have put reference counting back in close competition with tracing, but it's still somewhat slower. Reference counting offers one alternative, though -- the performance is deterministic. You have particular points in the code where destructors are injected, sometimes without a reference check (if the ORC/ARC optimization is good) and sometimes with a reference check, but you know your program will deallocate only at those points. This isn't the case for tracing GCs, where the garbage collector is more along the lines of a totally separate program that barges in and performs collections whenever it so desires. Reference counting offers an advantage here. (Also in interop.)

So, while you do need a cycle breaker to not potentially leak memory, Nim tries to get it to do as little as possible. One of these tools they provide to the user is the .acyclic pragma. If you have a data structure that looks like it could be cyclic but you know is not cyclic -- for example, a tree -- you can annotate it with the .acyclic pragma to tell the compiler not to worry about it. The compiler has its own (straightforward) heuristics, too, and so if you don't have any cyclic data in your program and let the compiler know that... it just won't include the cycle collector altogether, leaving you with a program with predictable memory patterns and behavior.

What these .cyclic annotations will do in Nim 3.0, reading the design documentation, is replace the .acyclic annotations. The compiler will assume all data is acyclic, and only include the cycle breaker if the user tells it to by annotating some cyclic data structure as such. This means if the user messes up they'll get memory leaks, but in the usual case they'll get access to this predictable performance. Seems like a good tradeoff for the target audience of Nim and seems like a reasonable worst-case -- memory leaks sure aren't the same thing as memory unsafety and I'm interested to see design decisions that strike a balance between burden on the programmer vs. burden on performance, w/o being terribly unsafe in the C or C++ fashion.

There is also a section related to performance available at the link I posted. Third header, "Likely Concerns", second subheader, "DoS/Amplification".

The only difference in visible replies is in the moderation choices of the server the post is viewed from.