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

Showing that program code refines a TLA+ spec has been done for C and Java (although scalability is a different matter).

C: http://link.springer.com/chapter/10.1007/978-3-319-17581-2_1...

Java: http://ieeexplore.ieee.org/document/6042069

The C work seems more thorough.

Amazing! I hadn't heard of this, thank you. I'll add it to the Wikipedia article.

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