romac

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!