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

Amenable? Probably fairly amenable. It hasn't been done yet, though. It likely wouldn't be translation so much as proving that the existing code refines a TLA+ spec.

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.

Applications are open for YC Summer 2018

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