Good question! There is an entire field of "formal" verification with associated conferences such as FMCAD, CAV, etc which has a long history, and the meaning has indeed changed over time. It may well mean different things to different people.
In general, to me, "formal" comes from "formal logic" and fully specified proof systems. In the field of verification, "formal" often means there is an associated proof of correctness or of unreachability say of a panic. But it has come to also mean bug-hunting tools such as cbmc <https://www.cprover.org/cbmc/> which are based on modelling C for bounded model checking. So some examples may be - SAT/MAXSAT/SMT solvers - verification tools like SLAM - modal logic solvers - Golang source analysers which produce models of source code execution and then prove things about them Some folks consider type theory formal, as in pure form (like system F, type systems for ocaml) "formal" as well. There are also things like proof carrying code which contains a proof that remote execution is safe in some way. so what "formal" is not formally defined :) Hopefully, this will help clarify for those without prior exposure to the field. Scott On Thu, 27 Sep 2018 at 11:42, Jan Mercl <0xj...@gmail.com> wrote: > On Thu, Sep 27, 2018 at 11:38 AM Scott Cotton <w...@iri-labs.com> wrote: > > > I've just created a github organisation for formal tools in and for Go. > > Please expand on what a 'formal tool' is. I have no idea. > > -- > > -j > -- Scott Cotton http://www.iri-labs.com -- You received this message because you are subscribed to the Google Groups "golang-nuts" group. To unsubscribe from this group and stop receiving emails from it, send an email to golang-nuts+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
