Formal methods only solve half my problems
brooker.co.za
brooker.co.za
https://blog.nubix.de/index.php/2022/04/06/testing-baremetal...
https://perspectives.mvdirona.com/2014/07/challenges-in-desi...
James isn't the architect of AWS either, the scale we're at and the way we organize ourselves mean we don't really have any single architects of anything. Also EC2, S3, SQS, and more were in place by the time James joined. But I'm not trying to talk down James, because James has been much more influential and important to AWS success than an architect! His technical and business insights, his vision and drive, and his focus on some really very key levers have been monumental drivers of AWS. I know I've learned a lot from him, and still do. He's so good at it that he's now on the Amazon leadership team, reporting directly to our CEO!
Thanks for the clarification though. This is truly why I enjoy HN so much. The ability to get corrected by the experts is an honor :)
Some features:
- open-source
- cross-platform
- quick editing with syntax highlighting, type annotations etc. in VS Code
- run in a single command (‘dotnet fsi script.fsx’)
- type-safe but with global type inference
- grab dependencies using directives in the script (no project manifests or global dependencies)
The added safety of a typed language is fantastic for scripting because it’s not worth writing tests for most scripts.
The downside: requires 1. installing stack and 2. waiting for it to install ghc and libs on first run of the script.
> Can there still be side channel attacks in formally verified systems? Can e.g. TLA+ help with that at all?
Side-channel attack https://en.wikipedia.org/wiki/Side-channel_attack
The use of constant-time algorithms for crypto is a way to mitigate things like timing side-channels, and there are other techniques like disabling hyper-threading that can help.
The depressing fact is that side channels exist any time there’s a shared computing resource. The question is how noisy the channel is, the data rate, etc.
Category:Side-channel attacks https://en.wikipedia.org/wiki/Category:Side-channel_attacks
Would formal methods help with code at this level?
I suspect the cost benefit isn't there. Though I wish it was. I've seen the difference between having tests and not having them. Development time decreases, and my stress levels decrease. Is this the same with formal methods?
That being said, FM is an enormous spectrum; if you squint a little, writing really good user stories could be considered a 'formal specification'. There's a really good paper from Amazon about model checking (Newcombe 2014 IIRC) where they make the bold statement that "Doing the math didn't help us find that many mistakes, nor did using the model checker; the thing that was most helpful was sitting down and forcing ourselves to come up with really good definitions. Like what does X really mean?" So it doesn't have to be as complicated as you think.
So if you want to start as simple as possible, I would recommend something like this: https://www.hillelwayne.com/post/decision-table-patterns/
There is also a more powerful version of Decision Tables called Tabular Expressions (from D.L.Parnas) which you can use.
A nice succinct reference to Formal Methods is Concise Guide to Formal Methods by Gerard O'Regan.
I think simplified versions of Formal Methods can be used profitably for your use-cases. Start with Assertions, Design-by-Contract and Decision Tables.
That is, formal methods aren't testing the code you write, just the design concept behind it. For the design concepts you are likely to encounter in your situations, you absolutely do not need a formal proof that your stuff works - unless you are inventing (e.g.) a new cryptography suite from scratch or a large distributed system that must handle a massive amount of concurrency, there is zero advantage you would get over following best practices.
It is verified implementation.
I'm not sure where this idea came from. Are you in hardware? I guess in hardware that makes sense.
Anyways, in software, formal methods can absolutely show that an implementation meets a specification. In fact, that has always been one of their canonical use cases in software systems, at least since the 70s or maybe early 80s.
Formal methods can also be used with very ad hoc specifications, or with very general specifications, or increasingly without any explicitly specification at all (eg by inferring specifications).
> cryptography suite from scratch or a large distributed system...
Or aerospace software, or automotive software, or certain financial software, or industrial control systems, or any complex billing/access control, or...
> there is zero advantage you would get over following best practices.
I wrote a bunch of static analyses that checked for common configuration errors in Django apps which saved us many weekends. YMMV.
> Anyways, in software, formal methods can absolutely show that an implementation meets a specification. In fact, that has always been one of their canonical use cases in software systems, at least since the 70s or maybe early 80s.
To be clear, I'm talking about systems that go beyond simple property validation. Presumably, we're both talking about e.g. Ada SPARK, Alloy, TLA+, etc. I would hesitate to call a type system a formal method, for example, unless they use some notion of tactics like Idris, Coq and Lean do.
Now there certainly exist formal methods that can show that a program meets a given specification and conforms to certain desirable properties. However, they cannot show that the program is bug-free, because many properties of a formally-verified system may be relaxed in real environments. When I say "sound", I mean the property of being bug-free.
In OP's case, it would not help the OP reduce the frequency of bugs pushing to production - it would only give them confidence that they meet the spec, which is usually not what people writing internal tools are worried about. For industries where being safety-critical is not necessary, there is simply no meaningful advantage provided by formal methods over regression tests, clean refactoring and validators. While you can certainly use them, the benefits are slim.
> Or aerospace software, or automotive software, or certain financial software, or industrial control systems, or any complex billing/access control, or...
These are safety-critical industries, where things like temporal correctness, multiprocessor safety and other attributes matter - essentially, where you can model your system as process calculi and must demonstrate some invariants hold over the lifetime of the system given a specification. That is absolutely the domain of formal methods and where some formal verification is needed for certification. These industries are also the ones where you can ensure both certified hardware and software, so that formal verification actually does detect correctness bugs beyond what an integration test does.
But OP has not said they are in any of these industries, and I don't think it's incumbent on me to be exhaustive in listing them when it's not core to OP's question. If OP's asking this question online instead of their colleagues, we can safely infer they're likely not in an industry that demands formal certification already.
It's quite difficult to look at systems like Dafny or {J,C}BMC, in particular, and say "they can only show a _specification_ is sound, but not the _implementation_.", since those systems are definitely saying something about the implementation.
Regarding "soundness", I think you're confused about terminology. I have no idea what it would mean for a spec to be bug-free; that seems equivalent to saying that a program is bug-free. Specs can have bugs for the same reason that implementations can have bugs.
Anyways, "sound" has a well-understood meaning that is quite different from the one you're imposing. Soundness is a property of the entire system, not of individual formulas (specifications). A formal system/tool is sound if the system only admits proofs of a formula F whenever F is valid in the semantics.
> But OP has not said they are in any of these industries, and I don't think it's incumbent on me to be exhaustive in listing them when it's not core to OP's question.
You're missing the point, which are the ellipses.
OP's question is "are formal methods worth it for me?"
The appropriate answer has NOTHING to do with the type of code that OP is writing or their application domain. AWS components are not safety-critical in the sense of aircraft or automotive software, and they run on commodity hardware. Ditto for financial systems. But formal methods are applied successfully in both contexts.
Again, I've used hand-rolled formal methods for Django apps as part of our deploy process and it's definitely saved us headaches.
The implementation effort took very little time. A weekend and then a bit of ad hoc follow-up work. The rise of amazing parsers, really good implementation languages for this sort of code (scala, F#, ocaml), and fantastic SMT solvers (particularly string constraint solving) means that what used to require a "huge investment" can now be done in a weekend hackathon. Hardware is also making formal methods a cheaper prospect. Lately I've been playing with a small cluster of 64 core processors during off-hours and the amount of brute force search you can do in a weekend is pretty incredible.
Formal Methods are often cheap and easy to implement, but they do have a high up-front human capital cost/learning curve. You need to know how to coalesce a class of bugs into a mathematical description. And then how to check that mathematical description against code by hacking together parsers, AST rewrites, and SMT solvers. The idea that this takes months or years of even weeks of time is pretty dated. A learned hand can get a lot done in a weekend.