3 ms·

I mentioned Lexifi, a contract language, which is based on OCaml and is not imperative. I restricted my argument to Europe as we appear to be less commerciall

• pron 10y ago
  > I mentioned Lexifi, ... which is based on OCaml and is not imperative. Oh, sorry. > we appear to be less commercially influenced I don't think this has anything to do with commercial influence -- just academic tradition and maybe even philosophical influences: I think you'll get different answers to the question, "does an algorithm or a computation exist outside its description in a language, and if so, in what way?" This may be tied to actual philosophies, Derrida in France vs. Kripke in the US[1] (to prove the connection, a "Kripke structure" is a very common mathematical structure denoting an "abstract" computation, which is used commonly in non-language-based verification). I've been told that the study of program semantics tries to reconcile the two. As to Haskell vs. Python, first, MIT used to teach Scheme; they have explained their reasons for switching to Python. Second, this difference is more indicative of the competition between "theory A" and "theory B". Theory A studies algorithms and complexity (and Haskell is not the best first pedagogical choice for that), while theory B studies logic and semantics (and language). Theory B is relatively small, but it does have a stronger presence in Europe. Although, even within theory B there seem to be those who prefer linguistic approaches (semantics) and those who prefer conceptual approaches (Kripke structures, abstract machines). [1]: Not that Britain is too fond of French philosophy, but the Brits had Robin Milner, who is as close to a CS deconstructionist as you could find.
  • willtim 10y ago
    It's worth pointing out that most of the formal methods you have linked to involve contracts or specifications as separate stratified layers written in various logics. No Turing Machines involved. This is essentially functional programming as far as I'm concerned. The advantage of the dependant-type approaches like Coq and Agda, is that the language of proof and implementation is now one of the same, but I was not necessarily advocating their use as you seem to have assumed. Even without dependent types, a total functional program can serve as both an executable specification and a logic with which one can derive proofs from (e.g. via an SMT solver). This is what I meant when I said functional programming is more amenable to formal methods. So any tool that uses dataflow analysis to convert imperative programs into functional ones, or requires me to write functional programs to describe what the imperative program should be doing, doesn't provide a counter argument in my mind. Finally, in my very first comment, I provided a link to a startup who are planning on using FP and SMT solvers for formal verification of blockchain contracts, so watch this space...
    • pron 10y ago
      > No Turing Machines involved. When are Turing machines ever involved? Verification tools often make use of abstract state machines as the subject of their study. I am not aware of a single one that deals with Turing machines (nor am I aware of a single TM programming language being used in the industry). TMs serve an important role in theoretical computer science, in automata theory and complexity theory, but not in verification or PL. > This is essentially functional programming as far as I'm concerned. It isn't. Logic was applied to programs long before FP was in vogue. > The advantage of the dependant-type approaches like Coq and Agda, is that the language of proof and implementation is now one of the same, Two things. First, you can implement a system in Isabelle, too. Second, that advantage -- if it is one -- is rather theoretical at this point. Dependently typed languages have never been used outside of the lab, and have never been used in a large project. The approach, BTW, has plenty of disadvantages. First, the languages are very hard to learn, and require some very exotic, obscure math; second, some very important properties like time and space complexity -- that are often just as essential as logical correctness for those application where correctness matters most -- are hard to express, and there's no consensus yet on how to best reason about them. In short, dependent type approaches may one day be useful, but in general, we're not sure exactly how to use them yet. > a total functional program can serve as both an executable specification and a logic with which one can derive proofs from That is absolutely true, but this has some very severe disadvantages as well. > so watch this space... I have no doubt. But you should be aware that FP approaches to verification are just some of the many avenues in verification research these days, and are not generally accepted to be the most promising ones. In addition, unlike other approaches, they have pretty much never been put to the test outside the lab. Finally, SMT solvers are successfully used to verify Java programs (with JML specifications), and in the research world, Microsoft's Dafny[1] -- an imperative, non-functional (I think) language -- is a very popular choice in verification challenges (alongside tools like KIV[2] and Why3[3]). They also, I think, serve as the core proof method of SPARK Ada, a heavy duty verifiable language, with a good track record over many years in the industry. [1]: http://research.microsoft.com/en-us/projects/dafny/ http://research.microsoft.com/en-us/projects/dafny/ [2]: http://www.isse.uni-augsburg.de/en/software/kiv/ http://www.isse.uni-augsburg.de/en/software/kiv/ [3]: http://why3.lri.fr/ http://why3.lri.fr/