5 ms·

Might want to show some examples in the "Why Not To Use Formal Methods" section too. Somewhat old numbers from seL4: [1] - 2,500 lines of C code - 100,000 li

• nine_k 7y ago
  Maybe C is just not the best tool for such code. I would suspect that (subsets of) Ada, or, Rust, or maybe OCaml would be more fitting while staying on the industrial side. (Likely Haskell or Idris would be even easier targets, but their industrial adoption is quite limited.)
  • tsimionescu 7y ago
    Why do you think so? I would expect the vast majority of the proof to be about the semantics of the OS, not about language-level details. Formally proving complex properties is just an inherently difficult and time-consuming task. That is the main reason it is not often undertaken, even in mathematics if I understand correctly.
    • SkyMarshal 7y ago
      It probably depends on your trust assumptions and requirements. Ideally we write formally provable code for a formally proven compiler to run on a formally proven OS/bios/hardware. But some use cases require safe client code that will nevertheless run on unsafe OS and hardware. Client-side and some server-side cryptocurrency apps are one example that comes to mind. Probably banking apps too. It's still useful to write them in strongly typed languages amenable to formal verification, even though they'll be running on unverified Windows, Linux, MacOS and smartphones. Also we really need OS's, firmware, etc. written in languages amenable to formal verification, but given the massive lockin of the mainstream options, that's a pipedream for now. But a worthy long-term goal.
      • tsimionescu 7y ago
        I'm not sure that there are languages more or less amenable to full formal verification. Formal verification of a system is such a complex task that the language-level details are unlikely to be a significant proportion of the effort. You can also look at existing formally verified software and probably confirm my assumption - there is likely as much formally verified C code (a weakly-typed, memory unsafe language) as formally-verified Haskell code. And I do not agree at all that a formally verified banking app is a good idea. It would likely be so difficult to do that by the time it is finished it no longer runs on any current version of any OS. Formal verification is just too hard to be worth it. There are better methods of ensuring software correctness that are far less costly. Maybe something will be discovered in the future that will make it easier, but for now formal verification of any piece of software more complex than a few hundred lines of code is a multi-year research-level project.
  • hwayne 7y ago
    The seL4 code didn't start out as C. First they wrote the whole thing in HOL (an ML dialect), then translated that to Haskell, then translated _that_ to C. Verifying code is correct is Just Plain Hard.
  • gindely 7y ago
    How does the industrial adoption of OCaml compare to Haskell? (The relative placement of Ada, Rust and Idris seems apparent.)
    • nine_k 7y ago
      I know two large companies using OCaml to a serious extent: Jane Street (obviously) and Facebook (as Reason). I can't remember any large company where Haskell would be front and center, but a number of smaller companies doing so exists. There was a post about running Haskell in production recently here on HN.
• rustybolt 7y ago
  Yup. This shows why we need languages that are more amendable to formal methods. Proving stuff requires you to write short code that is obviously correct. For most programs, an 'informal' proof would be a huge improvement already. The effort you have to put in non-formal proofs is much lower, but the main drawback is that they are not checked, so you might make mistakes in the proof (on the other hand, you can make mistakes in the specification as well). The holy grail would be formal methods that work mostly like informal proofs. With todays methods you would only prove the smallest, most critical parts of the code correct.
  • zozbot234 7y ago
    If you're going to write a formal spec in the first place, you can then "fuzz" the code against the spec, or parts of the spec against itself. I.e. try to find an automated refutation as opposed to a proof. Model checkers work according to this principle, and I assume that the combination of "informal" proof and automated model checking can be especially helpful for suitably-sized systems. Either one of these without the other seems a bit harder to take seriously.
• hwayne 7y ago
  Agreed- that's why I said in the beginning I'm only talking about design verification. Verifying code is a long way off from going mainstream. I talk about the limitations of code verification in this essay: https://www.hillelwayne.com/post/why-dont-people-use-formal-methods/ https://www.hillelwayne.com/post/why-dont-people-use-formal-...
  • zozbot234 7y ago
    I assume you mean "full" code verification in some sense. Partial verification, especially of properties that are "local" and where verification can be done in a way that's "based" on the language syntax itself, is relatively common. This kind of verification is often called "type checking" and is often not even thought of as a means of code verification. One can of course object that requiring the use of a language where verification is "baked in" like this might be undesirable; but either way, it seems clear even to formal-methods proponents that well-chosen language semantics are going to be very important if code verification is to be feasible. So it's six of one, half a dozen of the other.
• pron 7y ago
  This article talks about design specification and its model-checking; seL4 used a completely different formal method. Formal Methods (for software assurance) is the name of a research discipline studying the following methods, as well as programming language semantics: * Formal specification of either code or design * Model checking * Sound static analysis * Machine-checked/assisted deductive proof systems and dependent type systems * Concolic testing and automatic test generation * Program synthesis Some of the verification methods above (like some model checkers and sound static analysis) can be used without any explicit specification whatsoever (e.g. they're used to verify lack of undefined behavior in C programs). So the name "Formal Methods" covers a wide range of tools and techniques, with widely varying goals, costs and appropriate domains, that it doesn't really mean much to talk of "formal methods" as if it were a specific thing. Rather, it is a general approach used in constructing widely differing tools and techniques. That's why it's called formal methods, not a formal method.
• billfruit 7y ago
  I don't know why this strain of thought continues to have currency that formal methods are some kind of unattainable utopian ideal, this line of thinking is exactly what Dijkstra prophesied that the flawed CS education would lead us to think, that testing software is a viable option to ensure their correctness.
• ken 7y ago
  The (famously robust) SQLite has 92 million lines of tests, for 139 thousand lines of code. How many person-years did that take to create? And then there are the hundreds of software libraries I've seen throughout my career that I never got to use because they were just too buggy. From where I stand, C doesn't scale to significantly-sized codebases. Nobody I know uses it except when they need to glue to some legacy C code that's been tested in production for the past few decades. It's easy to say something is a lot of work, but in this case every one of the alternatives looks worse. I don't have the time or resources to write 1000x my program in test code, to debug it in production for 10 years, or to throw it all away because I never achieve a minimum usable level of quality. Formal methods aren't looking so bad to me right now!