I think a better question is: can go tools for formal verification become available? The distinction is that formal verification tools can be applied to hardware, protocols, assembly, software, etc. Why not do that in go?
Most such tools are in C or C++, and the low level engines/components are highly optimised. Go can easily compete with "standard" C/C++, i.e. software which has not been highly optimised. It also provides enough low-level access to be competitive against highly optimised C/C++ (e.g. assembly, precision of memory representations) but it takes work. One of the research initiatives we are taking up is "scalable cloud architectures for formal technologies". Basically, composable cloud microservices for formal technologies like model checking, SAT/BDD/SMT, theorem proving, as well as encoders for verification problems, etc, but in terms of deployment in the cloud. A related startup is satalia. Go is a natural fit for this initiative, and we already have some results with go. I think the biggest obstacle to formal tools targeting analysis of go programs is formal representations in the golang "go" package. Once that is available, things will start to snowball. Le lundi 9 mars 2015 01:07:36 UTC+1, Camilo Aguilar a écrit : > > I ran across this post today: > http://blog.adacore.com/testing-static-formal. Basically, showing how you > can do formal verifications in ADA2012. Is it realistic to think that a > feature like that would someday arrive to Go? -- 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.
