Hacker News new | past | comments | ask | show | jobs | submit login

It's not "getting around", and one could write an extraction tool like that for TLA+, too. The difficulty is simply verifying any system, by whatever method, end-to-end, namely verifying that the high-level global correctness properties are preserved all the way down to machine code. We simply have no idea how to do it for real-world, large software, and in those cases it's been done for small, simple software (seL4, CompCert), the process was extremely expensive.



Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: