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

> and then show that a particular sorting program is indeed an implementation of Quicksort.

I wasn't aware that TLA+ made this part possible. How do you map from TLA+ to C++ (for example) with certainty?

Oh, you usually specify in multiple levels of detail in TLA+ and relate them and only informally relate them to code, but if you want a formal relation to code you could compile your program to TLA+ (e.g. http://tla2014.loria.fr/slides/methni.pdf).

... But you probably don't really want to do that. Code-level verification using any "deep specification" tool (TLA+, Coq, Isabelle, Lean, F* etc.) is extremely limited in scale compared to specifying in TLA+ at a higher level. Because there is no known way to directly verify programs larger than several thousand lines affordably, and because that's precisely the kinds of programs that most engineers need to verify most of the time, it's far more common to use TLA+ at a higher-than-code level.

Refinement calculus is what it's formally referred to as. As pr0n has mentioned you start with a high-level, abstract model. You then create a second model that implies every invariant of the first while adding more detail. You proceed like this to get closer to the implementation. If you are satisfied they are one and the same you can stop.

However the goal isn't often to verify every single line of code. That would be prohibitively time consuming and expensive. The ideal use for this stuff is to verify the hard parts that are critical to get right. Verifying that a critical section of code will not lead to a deadlock or resource contention might be really important and so you could start with verifying that particular system.

Applications are open for YC Winter 2020

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