>
> I have registered
>
> https://scan.coverity.com/projects/libc-musl

"You are not authorized to access this page."
I have no experience with Coverity, but I guess you missed a step to make it public. (The search also comes up empty.)


​Yes, I noticed that as well. It gave me the same "not authorized" message. Normally, we should be able to add the project to our personal Coverity accounts by going to My Dashboard (top), click the Add a New Project button, then search for the project. Currently, musl is still not showing up in the search – maybe it takes a couple of days to show?

Nagy, everything you said sounds right. What about unikernels? Long-term, I'm more interested in running unikernels than in running Linux, BSD, or Windows. I'm thinking of something lik
e OSv
​, where they built an ELF linker from scratch, as well as implementing the Linux system calls: https://github.com/cloudius-systems/osv/wiki/Components-of-OSv

In their case, they were going for glibc compatibility, and I assume a straight musl implementation would be easier. This ultimately gets at the separation of OS syscalls and ABIs vs. the libc. What if I have an OS or unikernel that doesn't know anything about C or POSIX, where C isn't a first-class citizen so much as an honored guest? musl-leveraging C applications would presumably be statically compiled in that case (and perhaps containerized), but there would also need be an ABI layer that is unclear to me. (Maybe this is relevant: How to Run POSIX Apps in a Minimal Picoprocess: http://research.microsoft.com/apps/pubs/default.aspx?id=183461 -- which they might be drawing from in their recently announced bash or Ubuntu support. How they emulated the Linux ABI in that paper is very interesting.)

I think the formal verification task would be simplified if we could shrink the ABI down in a unikernel or similar context, but I've only just begun to think about this.

On floating point, the C
ompCert team just published a new paper on verified compilation of floating point computations:
​ ​
https://hal.inria.fr/hal-00862689
​  ​
It looks like nice work.

Cheers,

Joe