romac

The Rust compiler (rustc) is written in Rust, but there can always be bugs in the compiler, regardless of whether it's written in a memory-safe language or not.

FTL v0.1.0 was just released, adding async Rust support (multi-thread Tokio runtime) and lots of missing pieces in the Linux compatibility layer.

(not my project)

Yes there are many such crates, which can indeed kinda fill the gap. One of the more recent one is https://docs.rs/bon

There is a single-page version of the book that you can save as a PDF: https://betrusted.io/xous-book/print.html

You can also go the other way around and generate traces [1] from the TLA+ or Quint [2] specs using the Apalache model checker [3], map each action in the trace to an action on your system under test, and check that the abstract and concrete states match at each step.

[1] https://apalache-mc.org/docs/adr/015adr-trace.html

[2] https://quint-lang.org

[3] https://apalache-mc.org

If you are interested in TLA+, you might want to check out Quint (https://quint-lang.org), a modern take on a specification language which shares the same underlying temporal logic of actions, but with a syntax more familiar to programmers.

And they are pushing in that direction: https://machinelearning.apple.com/research/homomorphic-encry...

If you haven't seen those already, you might also want to check out:

  - Apalache: a symbolic model checker for TLA+ backed by Z3 (https://apalache-mc.org)
  - Quint: a modern and executable specification language with TLA+-like semantics, that integrates with Apalache (https://quint-lang.org)

I wonder if this could be made to work in the browser using CheerpJ?

https://cheerpj.com

Vale has a very interesting approach to memory safety, without garbage collection or a borrow checker, using a memory management technique called "generational references" which I had never heard of previously.

Great to hear, thanks!

Has anyone received that kit yet? What are your thoughts on it?

I like how Rust does it with the `Ordering` type and associated combinators: https://doc.rust-lang.org/stable/std/cmp/enum.Ordering.html

For two values `x` and `y` of the same type with fields `a` and `b`, this lets you compare on `a` first and then on `b` by writing

``` x.a.cmp(&y.a).then(x.b.cmp(&y.b)) ```

Direct link to the Apalache model checker: https://apalache.informal.systems/

You nailed it, that's exactly what we use Z3 for in Apalache, a symbolic model checker for TLA+: https://apalache.informal.systems

"From October 1 [2013], an adult caught smoking cannabis in Switzerland can escape formal legal proceedings by simply paying a fine."

http://www.swissinfo.ch/eng/swiss_news/Mixed_feelings_over_n...

There is indeed. Take a look at require.extensions:

http://nodejs.org/api/globals.html#globals_require_extension...

Here is another interesting C/Objective-C Q&A: http://www.eosgarden.com/en/articles/objc-quizz/

I would also have added http://codecs.ofmlabs.org which features hand-ported MP3 and ALAC decoders.

Reminds me of something :)

$ cat /dev/urandom | base64 -b 80 | lolcat

We just set another VPS up. Everything should work fin by now.

I just added the link song feature. The link above should now work ;) Enjoy!