3 ms·

When I first read the snippet, I thought "What a terrible piece of code.". Later on, I read: "In fact, the code written above was actually entirely automaticall

When I first read the snippet, I thought "What a terrible piece of code.". Later on, I read: "In fact, the code written above was actually entirely automatically synthesised by our tool, along with a proof certificate, formally guaranteeing its correctness." So it looks like the code is terrible, and they only give an example for a simple usecase. So I'm not very enthousiastic about using this technique in practice. The rest of the post looks very informative though, although I haven't completely read it yet.

zozbot234 5y ago
> So it looks like the code is terrible, and they only give an example for a simple usecase. Yes, I'm very skeptical about this being "the future of coding!" (quoting the OP). These tools typically get stuck as soon as one needs to deal with non-trivial loops or recursive code, because it's not clear how to "synthesize" the correct loop invariant or inductive hypothesis; in particular, this cannot be done "compositionally" or "step-by-step" as in the simple case OP demonstrates. Typically, a developer has to step in and provide the right invariant so that the tool can get unstuck. Proof synthesis has exact the same issue, so generating proof-carrying code is also something that cannot thus far be automated except in very simple cases. Having said that, separation logic can be a valuable low-level tool and has been used to assess the correctness of, e.g. Rust borrow checking, which aims to provide lightweight, composable guarantees that can scale up to encompass larger programs. Even there though, we're nowhere near an actual proof, and soundness issues have in fact cropped up in the past as new features got added.
- YeGoblynQueenne 5y ago
  >> These tools typically get stuck as soon as one needs to deal with non-trivial loops or recursive code, because it's not clear how to "synthesize" the correct loop invariant or inductive hypothesis; in particular, this cannot be done "compositionally" or "step-by-step" as in the simple case OP demonstrates. By "inductive hypothesis" do you mean the inductive case in a recursion? If so, I'm curious, why do you say this? My experience is that the problem with learning recursion is constructing the "base case", particuarly when there is no example of it. Do you have specific examples where the inductive case is hard to find when learning from specifications?

zozbot234 5y ago

> So it looks like the code is terrible, and they only give an example for a simple usecase. Yes, I'm very skeptical about this being "the future of coding!" (quoting the OP). These tools typically get stuck as soon as one needs to deal with non-trivial loops or recursive code, because it's not clear how to "synthesize" the correct loop invariant or inductive hypothesis; in particular, this cannot be done "compositionally" or "step-by-step" as in the simple case OP demonstrates. Typically, a developer has to step in and provide the right invariant so that the tool can get unstuck. Proof synthesis has exact the same issue, so generating proof-carrying code is also something that cannot thus far be automated except in very simple cases. Having said that, separation logic can be a valuable low-level tool and has been used to assess the correctness of, e.g. Rust borrow checking, which aims to provide lightweight, composable guarantees that can scale up to encompass larger programs. Even there though, we're nowhere near an actual proof, and soundness issues have in fact cropped up in the past as new features got added.

YeGoblynQueenne 5y ago
>> These tools typically get stuck as soon as one needs to deal with non-trivial loops or recursive code, because it's not clear how to "synthesize" the correct loop invariant or inductive hypothesis; in particular, this cannot be done "compositionally" or "step-by-step" as in the simple case OP demonstrates. By "inductive hypothesis" do you mean the inductive case in a recursion? If so, I'm curious, why do you say this? My experience is that the problem with learning recursion is constructing the "base case", particuarly when there is no example of it. Do you have specific examples where the inductive case is hard to find when learning from specifications?