1. 43

Intro

I think there’s enough formal methods fans posting and discussing this here that it’d be nice to have a specific tag for it. Some of the things it would cover:

  • Specification Techniques: TLA+, Alloy, Z notation
  • Model Checking: bisimulation, state machines
  • Verifiable Languages: SPARK, ACL2
  • Proof Techniques: Coq, Agda, Idris
  • Case studies

Similar Tags

  • programming, compsci: too broad
  • distributed, compilers: common targets of formal methods, but not the only ones, plus formal methods is a fairly small niche in these fields
  • testing: probably the closest, but primarily focused on unit testing, property-based testing, good practice, etc. I think most people into FM are also into testing, but it’s different enough that it could be super confusing to put “we formally proved this!” under testing.

Examples

Alternate name suggestions: verification, correctness

  1.  

  2. 15

    I would also find this useful, and it’s a tag I would follow. I’d prefer formalmethods to verification or correctness, because I think the former is a bit broader (though some people do admittedly use it in a more narrow sense). The latter two imply very “applied” work to me, while I’d personally like somewhere to sneak in formal work that isn’t directly applied to verification, like logic programming, automata theory, logical semantics, etc.

    These are a few articles I’ve submitted under the generic compsci tag that I think would fit at least a broad interpretation: 1, 2, 3, 4, 5.

    1. 4

      it’s a tag I would follow

      As a relatively new user, I may not understand the use of tags completely. It seems the default behavior is following all tags and the primary use is to filter by tag. Thus, the choice of tags should be primarily driven by the need of a few users, who want to hide a complete class of articles.

      1. 2

        There are per-tag RSS feeds

        1. 3

          In addition to that, I use them manually to catch up on a handful of subjects I find interesting, by clicking on the tag, e.g. /t/lisp. Sometimes I read lobste.rs often enough that I see almost everything that gets posted in every category (except a few I filter). But other times I’m away for a few days, and the tags are a useful way of checking if I missed anything good in the areas I care most about.

    2. 6

      Big fan, I’m really interested in the topic and have already submitted a few stories about it.

      1. 4

        Added.

        1. 2

          I’m a bit mixed on this. It’s all part of overall field of software verification. There’s many subfields: requirements, specification, modeling, proving, and lightweight analysis (eg static analysis). The methods may be ad hoc, semi-formal (eg UML), or mathematical (full formal). Might be distributed. May (Coq) or may not (SPARK) contain serious math. CompSci, government, or industrial usually with occasional work by hobbyists.

          Testing already has a tag since it’s so popular. Question is how to encompass the rest in a word or two. Several tags for different activities? One for Verification covering everything not related to testing? One for Software/System Analysis that covers whole spectrum of application? Or Formal Methods for all activities with formality but just call semi-formal stuff Programming, etc? The complexity of this decision is why I didnt ask for a tag. But Programming + Math might lead to people filtering lightweight stuff like TLA+ w/ PlusCal they might understand and use since it was way easier than they expected seeing Isabelle, etc.

          1. 5

            Yeah it’s a bit of a venn-diagram area, which makes it tricky. There’s a whole area of theorem-proving, for example, some of which is used for verification and some not. I use answer-set programming in my research, which is a hybridization of SAT/SMT-style finite solvers and logic programming, but not for verification, or at least not primarily for that. I model game mechanics in ASP to be able to query them, which could be used to verify certain behaviors, but which I actually use for exploratory design and procedural content generation. But you could use very similar tools for verification, so there’s a certain family resemblance here. My own interests lie on the side of it that could probably be comfortably called logic, but there’s a lot of verification that wouldn’t fall there. Not sure where exactly to draw these lines. I mean, even for pragmatic purposes; where to draw the lines philosphically doesn’t have to be solved here. :-)

            I personally conceive of this all as formalmethods, but in practice that term does seem very tilted towards software engineering and verification. I kind of want something that ecompasses formal models for various purposes, of which verification is one.

            1. 1

              Thanks for sharing those use-cases as that’s some neat stuff. They’re also great examples of how formal methods can inform a design or exploration instead of just being about perfect software. I probably need to toy with ASP at some point, too.

          2. 2

            Are we including things like Cleanroom Software Engineering in this tag?

            1. 2

              I’d just call it Programming since it’s a methodology for programming that doesn’t actually require formal verification. It’s certainly a formal method but designed for people who wouldn’t get that. Overlaps considerably with good, programming style. I’d avoid putting formal tag on it just so someone wouldn’t filter it thinking it would be useless to them like a “Programming with Proofs” paper requiring strong, math/logic background.

              1. 1

                I was thinking “Huh?” then saw you posted most of it a year or two ago. I’d say keep them coming but stay on practical papers or examples where possible. Shows relevance for readers who are curious about stuff or waiting until it’s practical to their needs. That’s been my strategy except occasional research result that was pretty interesting. Most of those get low reads/votes. So, I say stick with stuff where even the abstract tells you something practical and neat.

              2. -5

                What counts as using formal methods?

                An image of a soap powder box would be very appropriate for this tag.

                Or perhaps that is too up market for the snake oil salesmen of computing.

                1. 8

                  The examples quoted mostly involve application of mathematics, logic, or good modelling to software to prove properties of it. The track record of that field is really good. Especially in hardware. I don’t know why you’d use the term snake oil salesman in light of that. Best reserved for those peddling unproven bullshit.

                  1. 12

                    Given that you are calling researchers “snake oil salesman”, “intellectually dishonest”, “lazy”, etc, I don’t get the feeling that you are engaging in good faith. I know some of the CompCert team and they are honest people trying to make a difference in the world. I can’t respond directly to your posts because I can’t tell which of that sea of questions is sincere and which is rhetorical grandstanding. If you have a single, sincere question you would like to ask about proof assistants like Coq or formally verified applications like CompCert, I would be happy to answer it.