Viewing profile — specialgoodness

The Nelson-Oppen simplifier is a great piece of work, but it is not the first SAT solver. Boyer and Moore published their formally verified SAT solver in their 1979 A Computational…

As an insider and major user of this effort in ImandraX, I must say: Moonpool and OCaml5 concurrency have been an absolute game-changer! Awesome read.

Xavier Leroy as Lou Reed... :-) Don't forget the amazing theorem provers too, like Imandra ( https://www.imandra.ai/core ), HOL-Light ( https://hol-light.github.io/ ) and Rocq ( ht…

check out Imandra's platform for neurosymbolic AI - https://www.imandra.ai/

Beautiful! Imandra is a modern Boyer-Moore style theorem prover for higher-order functional programming (its logic is based on a typed higher-order subset of OCaml rather than Boye…

This is interesting work but it totally misses the boat when it talks about the current state of the art. They cite a 2014 version of the Goel-Hunt-et al formal x86 model in ACL2, …