1. 49

  2. 8

    As a total noob, on chapter 3 of the Idris book, I was surprised how much Idris feels like a tool for working programmers, rather than an academic exploration of new type theory. Lots of little touches added for developer happiness. Really enjoying it so far!

    1. 6

      I can recommend watching this talk by Edwin Brady about Idris:


      It becomes very clear many of the features like typed holes and the interactive compiler come from usability concerns.

      This also shows here: Even though this 1.0 announcement makes it clear that Idris is still a research language, it also makes clear that they want to hold platform guarantees. That gives a lot of value for further research, based on a stable foundation!

    2. 5

      I’m looking to add some formal methods into my workflow, and it’s a tossup between climbing the Alloy, CoQ, TLA+, or Idris learning curves.

      1. 18

        I think it really depends on what you want to use it for. Here’s an extremely misleading overview of the use cases:

        • Coq: Good for writing mathematical proofs. “Does my proof of the P=NP have any errors?”
        • Alloy: Good for topologies and static structures. “Can someone be their own grandchild?”
        • TLA+: Good for state machines and concurrent systems. “Can we guarantee all uploaded data will eventually be processed?”
        • Idris: The only one of the four that’s an actual programming language.

        Personally I’m biased towards TLA+, because that’s the only one I know, but Idris is on my list and I’ve been making bedroom eyes at Alloy.

        1. 21

          Good except that Coq, although made for mathematical proof, is probably the most widely-used for verifying algorithms for programming problems that are usually then extracted into programming languages like Haskell or Ocaml. Almost all the best work on verified programs, from OS’s to compilers, is done with Coq or HOL. I’m not saying it was ideal choice for that but that’s what they’re using. Lots of stuff to build on, too, like Bedrock, CompCert, and protocol models. On HOL side, AutoCorres, CakeML, and Verdi come to mind.

          People should also look into K Framework & Maude for the rewriting/equational logic side of things. Those get too little attention despite how easily many problems are solved in them. Then there’s B method and Event-B with refinement if anyone wants to go all out on turning algorithms or systems into verified code. Gonna be work like Coq or HOL, though, since refinement is always a pain. Finally, Abstract State Machines if you really just want specifications not proofs as they’re easiest to learn and most successful in industry. I’m recommending TLA+ over it as it has more tooling & educational resources now days w/ similar capabilities.

          1. 2

            Verdi (the distributed systems proof system, including the proof of raft’s safety) was done in Coq. If you mean a different Verdi I apologise in advance.

            1. 1

              I misremembered it. You’re right. It was security protocols and clocks in HOL. Verdi used Coq.