> Hell, it makes me want to open the IDE and prove something right now. It makes me want to do a little bootloader development too... in Coq! It might be fun

> Hell, it makes me want to open the IDE and prove something right now. It makes me want to do a little bootloader development too... in Coq! It might be fun to make a tiny 16-bit real mode OS with this also. You could head towards your own miniature version of SeL4 os something. Edit: Oops! I forgot that it couldn't produce 16-bit machine code. Still, build a tiny bootloader that grabs the next sectors from the boot medium, then jump into protected mode (pretty easy really) and you are good to go!