(I am no expert in the analytic underpinnings of the beta distribution or precisely how it is the conjugate prior to the binomial -- or, rigorously speaking, what conjugate prior means -- but the formula here lines up with his formula :P )
Thanks for the feedback! I wasn't particularly dedicating this to new users. This solves a problem for me, an experienced *nix user. I'm not even sure it /would/ solve a problem for new users (arguably ninite doesn't either) - you need to know what packages you care about in order to have an interest in downloading them.
This site gives me an interface to say, "oh yeah, I /do/ need VLC on this laptop, come to think of it", rather than having to lazy-evaluate that when I have a video downloaded and realize I don't currently have a means of playing it.
I spend a fair bit of time doing DevOps work, and this isn't meant to be some sort of configuration management or provisioning tool. This is for desktop / dev users, which is, I think, quite a different use case (but an increasingly relevant one). I have a dotfiles repo, which is to say I'm familiar with the "document things in scripts and repos" game - but it's not clear to me that something like a script-as-documentation is even a useful process to go through when any given computer I set up is going to be used differently. That laptop playing VLC is very different than the web dev box I spin up to mess around with a new project.
The motivation was basically a version of ninite[1] for Linux. So very desktop-focused. I actually got in touch with the ninite folks, who used to run a Linux installer [2]. They said there wasn't enough interest and package managers are "good enough." I respectfully disagree on that point - I think that having the ability to point-and-click for the core, most important packages you want to install is really useful when you're spinning up a new desktop from scratch.
I was running into this problem after basically doing ad-hoc setup for every new machine I turned on. Sure - I could write a shell script / list of packages and save it to my dotfiles repo, but where would the fun be in that? :)
(Plus, package lists on every machine are different)
A few good ones here - another really interesting, current initiative is Bolsa Família, a Brazilian assistance program that functions similarly to a basic income subsidy - the main difference is that it requires families to demonstrate up-to-date immunizations and good school attendance rates for children.
The issue here is the spec - no runtime errors at the source code level is, as I understand, a completely different specification than end-to-end implementation correctness.
In particular, the Muen Kernel report itself [1] explains:
By implementing the kernel in SPARK and proving the absence of runtime errors, we have
shown that the kernel is free from exceptions. While these proofs provide some evidence to
the correctness claim of the implementation, the application of these particular formal methods
do not provide any assurances beyond the error free execution of the kernel. Proving functional
properties such as the correspondence of the scheduler to a given formal specification is necessary
to further raise the confidence in systems based on the Muen kernel.
In other-words, we don't yet have formal confirmation that this thing actually does what we might expect it to - just that its execution is bug-free.
But in the other direction, it seems that end-to-end implementation correctness implies absence of run-time errors. The seL4 authors write[1]:
> IMPLICATIONS [...]
a functional correctness proof already has interesting implications for security. If the assumptions listed in Sect. 5.5 are true, then in seL4 there will be:
No code injection attacks [...] No buffer overflows [...] No NULL pointer access [...] No ill-typed pointer access [...] No memory leaks [...] No non-termination [...] No arithmetic or other exceptions [...] No un-checked user arguments [...] Aligned objects [...] Wellformed data structures [...]
And this was already done in 2009. So I don't think Muen is the first microkernel to prove absence of run-time errors. (Maybe they claim that Muen is the first open source run-time-error-free microkernel in the sense that they did the verification after seL4, but before seL4 was open-sourced?)
I would guess so, seL4 was open sourced in August 2014 and the first public preview of Muen was December 2013, per a quick check with Google.
On the other hand, I've read that if you want to do serious SPARK/Ada work, you've got to buy AdaCore's tools or benefit from their academic program. seL4's verification down to binary was done using generic GCC (a clever way was found to meet the higher level proofs with stuff generated from the binary; they first tried CompCert (a verified C compiler that is free for non-commercial use) but I gather that suffered from an impedance mismatch).
Lots of free guides, tips, libraries, etc. You get way better tools in terms of testing, inspection, analysis, etc if you buy them. No doubt. The base platform, good enough for Muen or IRONSIDES DNS, is free. You can replicate their work easily plus create safer variants of established software such as Nginx, etc.
Whereas seL4 relies on Haskell, Isabelle, several proof frameworks/tools, C, and GCC. They achieved a lot more but with a lot more tools, time, and expertise. Those of us that were interested couldn't even check the verification stuff, especially the C-related tech, until late 2014. Using them would be... non-trivial to say the least. :)
Good that they open-sourced as that will allow (is allowing) others to build on the work. I know it's already getting integrated into Genode OS.
As I was told in a HN discussion that non-educational "for GPL" version doesn't supply the same runtime, and the run time supplied is not very good. Maybe it's OK, but with all those restrictions and limitations it just didn't sound like an ecosystem I want to mess with. Plus I prefer to be able to develop and release software with less restrictive open source licenses.
WRT seL4 vs. Muen, I wouldn't be surprised if seL4 does less for you, it's only 9,000 lines of C code, and some of it is artifacts from the manual Haskell -> C translation.
Ahhhhhh. Wasn't aware of that. Will have to check with them. Muen uses the zero-runtime profile. Not sure about IRONSIDES. Far as those using a runtime, if that's the case, I'd recommend some FOSS people create an alternative one that is good. Then they get the language, toolset, etc benefits without that issue. Recreating those will be much more difficult.
"WRT seL4 vs. Muen, I wouldn't be surprised if seL4 does less for you, it's only 9,000 lines of C code, and some of it is artifacts from the manual Haskell -> C translation."
That's not what I meant. seL4 is a separation kernel: they're supposed to do almost nothing. The thing is that once a modification occurs, it can invalidate the whole security claim. So, the person modifying it needs to be able to correctly use whatever its assurance depended on. That will be much easier for Muen given a domain expert only needs to learn Ada/SPARK vs all that went into seL4.
Now, Muen certainly has less assurance in that it doesn't have formal models of design, security policy, etc. Most FOSS types won't do all that, though. So, just requiring a language that knocks out errors and maybe learning Design-by-Contract is a nice alternative that might get more people involved. That it's Ada... might get less people involved. Who knows. (shrugs)
Exactly. It is exactly equivalent to saying that if a strict FP program compiles it is "bug free" but of course it has little to say about whether the code is 'correct'.
To me, the interesting bit here is that you have to be honest with yourself about your limits as well - and in particular, be very good about understanding those limits.
I think in this instance, ethics and economic incentives align - your expertise is part of your value-prop to clients, and having a good grasp of your limits makes you substantially more valuable. You get things done on-time, with clear expectations set, and do a prompt and thorough job providing what you're being paid for.
Personally, as a natural optimist, one thing I need to be especially careful about is not saying "yeah that's doable!" and setting expectations too high - it can potentially lead to a messy situation. That said, one of my favorite parts of freelancing is that I get confronted with new, unique challenges that I've never dealt with before - there's a balance to be struck here.
This confused me as well, since I've always used the normal central-limit-based confidence interval for binary outcomes.
[1] https://en.wikipedia.org/wiki/Binomial_proportion_confidence...
(I am no expert in the analytic underpinnings of the beta distribution or precisely how it is the conjugate prior to the binomial -- or, rigorously speaking, what conjugate prior means -- but the formula here lines up with his formula :P )