4 ms·

I know I've posted this a few times but I don't think I've ever seen you in a thread about this. Do you have any simple way for a computer scientist to learn ab

I know I've posted this a few times but I don't think I've ever seen you in a thread about this. Do you have any simple way for a computer scientist to learn about proven methods. More precisely, how do I engage in the dark incantations required to conjure up my own proven methods? For my critical code, right now I just write unit tests. Do you know some place that can shed some light as to what I actually do? I mean, I can just tell my coworkers "yea I formally proved this, it won't have bugs" but I don't think that's quite in good spirit.

aban 10y ago
Not the parent, but indeed like you said, writing unit tests doesn't show absence of bugs, but can only show their presence. To be able to state that a piece of software is bug-free and formally correct, we first need a notion of correctness: that the algorithm follows a [formal] specification. The first step would be to formally specify what the software/algorithm should do. Then, the next step would be to use formal methods and mathematical tools (e.g. set theory and logic) to prove that your algorithm does exactly as the specification says. TLA+ is a formal method that can be used for writing specifications and model-checking them. While a big step forward from testing, model-checking still doesn't "prove" anything. For proving, you can use theorem provers like the Z3 [0] SMT solver (or a formal framework that uses theorem provers) to do proof checking. The Event-B [1] method is one such formal method that uses SMT solvers and allows you to model systems starting with a very abstract and high-level model, state invariants about your system, and prove that those invariants hold as you refine your models and make them more concrete. Feel free to shoot me an email if you like to talk more about formal methods :) [0]: https://github.com/Z3Prover/z3 https://github.com/Z3Prover/z3 [1]: http://www.event-b.org/ http://www.event-b.org/
throwaway729 10y ago
What programming language(s) do you typically use for your critical code?
- gravypod 10y ago
  My next "big" project will be a data visualization system that's probably going to need some Python, JavaScript, and some simple bash piping between the python scripts. It's not going to be mission critical but it'll be nice to flash and say "I used formal methods to prove this implementation" as it is going to be for an academic's project.
  - throwaway729 10y ago
    > My next "big" project will be a data visualization system that's probably going to need some Python, JavaScript, and some simple bash piping between the python scripts. Unfortunately, there aren't great deductive verification tools for either Python or JavaScript. Perhaps more importantly, there's also not a particularly good understanding of how to formally verify front-end code. The most important property of a visualization system is something like "the visualization accurately represents the data being visualized", but in a problem domain like this, formalizing the high-level intent is probably harder than actually proving that this intent is achieved. Additionally, the cost of throwing an exception at runtime are presumably pretty low (unlike in a control system, for example). So once you've formalized your spec, you can just check your specs at run time throw an exception/report a bug instead of or in addition to generating the possibly faulty visualization. Are there key components of the visualization pipeline that could threaten its correctness? E.g. data reduction, interpolation, fancy graphics code, etc.? If so, I'd focus on those and come up with a good set of formal, checkable-at-runtime contracts that capture your high-level informal specification. Alternatively, is it possible to do some computation on your output to check that it matches the input data? E.g. you could imagine counting pixels of certain colors on a heat map or pie chart and comparing that to the original data. That way you don't have to verify (or trust) all of the graphics generation code, thus significantly reducing your trusted computing base. Saying "we have a formal mathematical description of what it means for this portion of the visualization system to be correct, and a way of checking input/output matches that description" is probably a more significant contribution than actually churning through a static verification effort. > it'll be nice to flash and say "I used formal methods to prove this implementation" as it is going to be for an academic's project. Are you sure this is the case? Most academics, even within CS, don't care much about formal methods. If you're just looking to learn formal methods, then I guess it's whatever. But if you're looking to stand out, you might want to figure out what's important to your stake holders and focus on that. I'd be pleasantly surprised if the answer to that question is formal methods.
munin 10y ago
Software foundations: https://www.cis.upenn.edu/~bcpierce/sf/current/index.html https://www.cis.upenn.edu/~bcpierce/sf/current/index.html VST: http://vst.cs.princeton.edu/ http://vst.cs.princeton.edu/ Dafny: http://rise4fun.com/Dafny/tutorial http://rise4fun.com/Dafny/tutorial You are probably not going to get to the point of being able to tell your coworkers "yes, this is formally verified" unless you are working in a specific domain where you have few/no libraries and very clearly stated and well trusted assumptions about the external environment (hardware, etc).

aban 10y ago

Not the parent, but indeed like you said, writing unit tests doesn't show absence of bugs, but can only show their presence. To be able to state that a piece of software is bug-free and formally correct, we first need a notion of correctness: that the algorithm follows a [formal] specification. The first step would be to formally specify what the software/algorithm should do. Then, the next step would be to use formal methods and mathematical tools (e.g. set theory and logic) to prove that your algorithm does exactly as the specification says. TLA+ is a formal method that can be used for writing specifications and model-checking them. While a big step forward from testing, model-checking still doesn't "prove" anything. For proving, you can use theorem provers like the Z3 [0] SMT solver (or a formal framework that uses theorem provers) to do proof checking. The Event-B [1] method is one such formal method that uses SMT solvers and allows you to model systems starting with a very abstract and high-level model, state invariants about your system, and prove that those invariants hold as you refine your models and make them more concrete. Feel free to shoot me an email if you like to talk more about formal methods :) [0]: https://github.com/Z3Prover/z3 https://github.com/Z3Prover/z3 [1]: http://www.event-b.org/ http://www.event-b.org/

throwaway729 10y ago

What programming language(s) do you typically use for your critical code?

gravypod 10y ago
My next "big" project will be a data visualization system that's probably going to need some Python, JavaScript, and some simple bash piping between the python scripts. It's not going to be mission critical but it'll be nice to flash and say "I used formal methods to prove this implementation" as it is going to be for an academic's project.
- throwaway729 10y ago
  > My next "big" project will be a data visualization system that's probably going to need some Python, JavaScript, and some simple bash piping between the python scripts. Unfortunately, there aren't great deductive verification tools for either Python or JavaScript. Perhaps more importantly, there's also not a particularly good understanding of how to formally verify front-end code. The most important property of a visualization system is something like "the visualization accurately represents the data being visualized", but in a problem domain like this, formalizing the high-level intent is probably harder than actually proving that this intent is achieved. Additionally, the cost of throwing an exception at runtime are presumably pretty low (unlike in a control system, for example). So once you've formalized your spec, you can just check your specs at run time throw an exception/report a bug instead of or in addition to generating the possibly faulty visualization. Are there key components of the visualization pipeline that could threaten its correctness? E.g. data reduction, interpolation, fancy graphics code, etc.? If so, I'd focus on those and come up with a good set of formal, checkable-at-runtime contracts that capture your high-level informal specification. Alternatively, is it possible to do some computation on your output to check that it matches the input data? E.g. you could imagine counting pixels of certain colors on a heat map or pie chart and comparing that to the original data. That way you don't have to verify (or trust) all of the graphics generation code, thus significantly reducing your trusted computing base. Saying "we have a formal mathematical description of what it means for this portion of the visualization system to be correct, and a way of checking input/output matches that description" is probably a more significant contribution than actually churning through a static verification effort. > it'll be nice to flash and say "I used formal methods to prove this implementation" as it is going to be for an academic's project. Are you sure this is the case? Most academics, even within CS, don't care much about formal methods. If you're just looking to learn formal methods, then I guess it's whatever. But if you're looking to stand out, you might want to figure out what's important to your stake holders and focus on that. I'd be pleasantly surprised if the answer to that question is formal methods.

munin 10y ago

Software foundations: https://www.cis.upenn.edu/~bcpierce/sf/current/index.html https://www.cis.upenn.edu/~bcpierce/sf/current/index.html VST: http://vst.cs.princeton.edu/ http://vst.cs.princeton.edu/ Dafny: http://rise4fun.com/Dafny/tutorial http://rise4fun.com/Dafny/tutorial You are probably not going to get to the point of being able to tell your coworkers "yes, this is formally verified" unless you are working in a specific domain where you have few/no libraries and very clearly stated and well trusted assumptions about the external environment (hardware, etc).