Every story and comment from the Hacker News API, in a layout borrowed from 2001.
A comment on Writing correct lock-free and distributed stateful systems in Rust, with TLA+. Parent comment
Here's the one I was referencing with the tiny TCB:
https://www.cs.princeton.edu/~appel/papers/flit.pdf
OK. So, it was a few Kloc. Still smaller than Coq. They could probably get it even smaller with recent work given translation validation knocks compilers out of TCB. So, in between 803-2668loc.
There are no comments on this comment yet.
Here's the one I was referencing with the tiny TCB:
https://www.cs.princeton.edu/~appel/papers/flit.pdf
OK. So, it was a few Kloc. Still smaller than Coq. They could probably get it even smaller with recent work given translation validation knocks compilers out of TCB. So, in between 803-2668loc.