I’m very excited to see that their first item, scheduled for Q4 2015, is 64-bit x86 support. Even without multicore, that’ll at least make it reasonable for anyone interested to start developing a userspace against it. I guess that’s on their roadmap for further down, anyway, but I’m impatient to play with it. :)
Anyone understand what’s going on with “Development Roadmap” and “Verification Roadmap” having separate dates? x64 is under development for Q4 15 but under verification for Q1 17 - is the C code going to be written without the associated proofs?
Oh, wow. I didn’t notice that. I believe your interpretation is correct; the C and the Isabelle code are both large amounts of work.