cmrx64

49 ms·

571.
by cmrx64 11y ago
Drivers will be pure Rust. Someone else can port a BSD to run on seL4 if they want.
572.
by cmrx64 11y ago
I know the website isn't terribly clear right now (it was posted a week earlier than I planned), but the first goal listed is exactly this.
573.
by cmrx64 11y ago
I have plans slated for doing proofs about Rust programs in 2017, if not sooner (I'm interning at Data61 on the seL4 verification team starting in two weeks, and if I don't get a chance to work on Rust verification then, I'll
574.
by cmrx64 11y ago
You've got it exactly right. AFAIK Linux can already be run in userspace on seL4, and there is also a VMM. This is a different project.
575.
by cmrx64 11y ago
Multicore support + verification is in the works, see https://ssrg.nicta.com.au/publications/nictaabstracts/Peters...
576.
by cmrx64 11y ago
Hi, project lead/main/pretty much only developer ( ;) ) here. I didn't plan on posting this for another week :( There's a bunch of stuff that still needs doing, especially with docs and tutorials. The writing on the webs
577.
by cmrx64 11y ago
The "Secure Enclave coprocessor" on the iPhone runs a modified L4.
578.
by cmrx64 11y ago
It's /only/ 30 man years of effort from experienced engineers. http://ssrg.nicta.com.au/publications/nictaabstracts/Klein_A... page 56.
579.
by cmrx64 11y ago
You can already use Rust on seL4, today! It's not ready for public consumption yet since there are no docs, but I've been working on it a lot recently and hope to have a release of the foundational libraries sometime in the next t
580.
by cmrx64 11y ago
Already done :)
581.
by cmrx64 11y ago
> The correct solution of course is just to use a memory safe language. Memory safety isn't enough, you need more. (More reading: https://microkerneldude.wordpress.com/2013/05/03/closing-the... ) Even
582.
by cmrx64 11y ago
(The author uses "her" in her biography section)
583.
by cmrx64 11y ago
This seems to be aimed more at humanities degrees than mathematics or computer science or other such technical degrees. I do still think applies in some cases to some jobs. Edit: looking at another post, http://blog.penelopetrunk
584.
by cmrx64 11y ago
Me and some other people are working on a seL4-based OS in Rust. We're getting ready to publically announce our first milestone by next week. There's also https://github.com/thepowersgang/rust_os , which is on
585.
by cmrx64 11y ago
And, before you know it, we'll have realized the dream of Urbit, in JS ;) Always bet on JS!
586.
by cmrx64 11y ago
Wow! The integration with rayon for data parallelism is especially interesting, and I imagine that could be a killer feature for some people looking to accelerate compute-heavy node.js code without having to deal with the nastiness of paral
587.
by cmrx64 11y ago
IME there's only an hour or so of downtime each month.
588.
by cmrx64 11y ago
gitlab.com really is awfully slow, but I don't know how that reflects on smaller deployments.
589.
by cmrx64 11y ago
I'm also a phan, but phabricator is more complex than GitLab and doesn't have (to my knowledge) a free, hosted version like gitlab.com. It also isn't quite as appropriate for open source projects, in my (admittedly somewhat l
590.
by cmrx64 11y ago
Just because it's irrelevant for real implementations doesn't mean it's not theoretically irrelevant. All of our computers can be modeled with sequential logic. That doesn't mean it's worthless to study more abstrac
591.
by cmrx64 11y ago
To me, I would have called that an "O(n^2)" (or whatever the proper non-linear order is) issue. The issue isn't that the algorithm is O(n), but that it's not O(n) when it could be! The other interpretations by andrewayle
592.
by cmrx64 11y ago
Isabelle's tutorial is quite comprehensive, and, I think, rather approachable to an ITP beginner: http://isabelle.in.tum.de/dist/Isabelle2015/doc/tutorial.pdf It assumes some knowledge of basic functiona
593.
by cmrx64 11y ago
Does anyone know what an "O(n) issue" is? I can think of a few possible meanings in the usage here, but I've never heard it before and they all seem wrong.
594.
by cmrx64 11y ago
I love love love tiddlywiki. I've been using it for probably 6 or 7 years now. It's simply amazing.
595.
by cmrx64 11y ago
We were a group of mostly undergrads. Computer Science students. What we did was meet once a week to discuss the reading and the exercises, or work through the exercises together. During the week we'd read the next few sections and try
596.
by cmrx64 11y ago
Ah, I see what you mean. Software Foundation hints ever so slightly at more specific approaches. Looking into the other books a little bit more, I'm not so certain Software Foundations would serve as a good introduction to them. The re
597.
by cmrx64 11y ago
Works for me now, at least.
598.
by cmrx64 11y ago
I've worked through TaPL too. I'm not even sure they are comparable :) It's possible to formalize the contents of TaPL in these systems (and, indeed, Pierce has taught it like that). But it's still a very different focus
599.
by cmrx64 11y ago
This is a lovely book. I gathered a group of students to work through this book last year (and even roped in a professor). If you're interested in formal software verification or interactive proof assistants, this is an excellent and a
600.
by cmrx64 11y ago
https://translate.google.com/#fr/en/coq , click "listen". Or, in French IPA ( https://en.wikipedia.org/wiki/Help:IPA_for_French ), kɔk (roughly transcribed to English, "couk"

More ›