Hacker News Reader

A while back I was exploring the use of 'soft' formal methods to help in evaluating correctness of some new modules we had to develop. I had come upon Alloy, which seems like a gentler introduction to formal methods (Unlike Z or Coq).

http://alloy.mit.edu/alloy/

Anyone have any experience using Alloy, or some other formal method?

View on HN

I've used it several times but the big problem with it is that once you have a nice, correct model that has been checked (and no counterexamples found), there's no way to translate it to code. This meand that your basically back on square one in terms of implementation.

I really like (and use quite often) the ASM method instead.

More of my thoughts here: http://ortask.com/how-i-designed-built-and-tested-a-temperat...

There's actually been imperative extensions and prolog compilers for it. Here you go:

https://homes.cs.washington.edu/~emina/pubs/alloy.mscs13.pdf

Also, for ASM's, the most interesting one I've seen is certified compiler project that is taking a lot less lines of code than CompCert:

https://www.complang.tuwien.ac.at/andi/papers/hipeac14.pdf

Reply on news.ycombinator.com