jesse_m

I love this app. I really like how it shows you tracking images and stuff in the emails.

Radicalized is in paperback on Amazon: https://www.amazon.com/Radicalized-Cory-Doctorow/dp/12502292...

It has unauthorized bread in it.

Also, he gets more of a cut if you buy from him and no DRM! win-win

One thing that seL4 requires is an mmu in order to support the isolation claims. The intel me type cpu would need to have some of these features that micorcontrollers don't usually have.

That's not necessarily true. There are VMM or hypervisor projects that utilize seL4 for x86 and ARM [1][2][3]. In this situation there isn't really one that is in "control". You could also have other threads or components that have higher privileges that can maybe do other monitoring or control activities.

1: https://github.com/seL4/camkes-vm 2: https://github.com/seL4/camkes-vm-examples 3: https://github.com/SEL4PROJ/camkes-arm-vm-manifest

For what it's worth, the current draft of the hypervisor extensions is available here: https://github.com/riscv/riscv-isa-manual/releases/download/... and is Chapter 5

It does say this: The hypervisor extension has been designed to be efficiently emulable on platforms that donot implement the extension, by running the hypervisor in S-mode and trapping into M-modefor hypervisor CSR accesses and to maintain shadow page tables. The majority of CSR accessesfor type-2 hypervisors are valid S-mode accesses so need not be trapped. Hypervisors can supportnested virtualization analogously.

Is the ports system similar to Gentoo's portage/ebuild system? I can get sources, configure the build, or get binaries (for some things) pretty easy through it.

The QA with the build farm would be nice though.

I can't stand the invisible syntax like double trailing space.

I can't stand the invisible syntax like a double trailing space is some valid syntax.

I think one of the big things here is that the refinement proofs from the models for isolation, IPC fast path, capability access control, and scheduling to C source to binary are strongest when the kernel is built with a particular configuration on particular hardware. When all of these are satisfied and you are on a trusted platform, you have very very strong guarantees that what is modeled is what you get. But it's not like this is hidden. They have make it pretty clear what the verified platforms and configurations are[1].

You should take a look at the verification chain though[1]. It is fairly extensive. It's not like they proved just a small part of a system in a general way.

1: https://docs.sel4.systems/Hardware/

2: https://github.com/seL4/l4v

The RISC-V proof is very close to being completed too. Gernot talked at the RISC-V Summit 2019: https://www.youtube.com/watch?v=2IXBoVIUuVI

I believe this was the HACMS program. Data61 has some more information: https://ts.data61.csiro.au/projects/TS/SMACCM/

It may be worth mentioning that it isn't the kernel that rebooted the system but some monitoring thread.

I think he's talking to the serval mesh guy

I haven't heard of the leo editor. I have used org mode in Emacs for little things. I also came across a reimplmentation of the tangling functionality: https://github.com/thblt/org-babel-tangle.py

The Embedded Muse http://www.ganssle.com/tem-subunsub.html

Jack Ganssle has some really good content he's written for other publications as well.

Looks like there are some open source mail server projects that support it: https://jmap.io/software.html

Is this similar to Android repo tool?

Also Google's repo tool. I like the idea of manifests and the commands it includes for creating feature branches across repos

fwiw, the Embedded Rust Working Group moved to matrix: https://rust-embedded.github.io/blog/newsletter-18/

how will we express the scale of something now?

I thought that when only web extension plugins were allowed shortcut extensions no longer worked. I was using keysnail. I was following https://bugzilla.mozilla.org/show_bug.cgi?id=1215061 but didn't know if it had been resolved. Thanks I'll check that out

can you browse without signing up? I'd like to follow from my mastadon client

Does this mean that custom emacs/vim keybindings can work again?

I do believe Western Digital is going to start shipping their products with RISC-V processors soon

If you use duck duck go as your search engine I think you can use their bang search functionality

Yeah I'm familiar with OCaml I wasnt sure if there was a language progression that was suggested to go through. I was actually interested in using Menhir more too.

Is there one of these languages to start with? Or would you choose one that interests you and study that one? There seems like some great content but I don't see a clear place to start

I've been looking at this too bit where do you source the wave guides?

Thanks I was using Tusky but had the wrong format for the name

Ahh thank you. I had the format wrong there