Thread

Loading the complete thread in the background. This saved snapshot is available now. Refresh

1. greatgib · 1789642177 · focus · HN ↗

   If anyone wondering, because it took me a few hops to find out:

   Z3 is a high-performance theorem prover being developed at Microsoft Research.

   1. Bluestein · 1789643149 · focus · HN ↗

      Or a BMW, or a groundbreaking electro mechanical computer, depending :)

      1. number6 · 1789643652 · focus · HN ↗

         I was hoping for the mechanical computer...
   2. 112233 · 1789643836 · focus · HN ↗

      oh, something new! I thought Z3 is SAT/SMT solver, they must have added something.

      1. Jaxan · 1789643934 · focus · HN ↗

         Sometimes you can use SMT for “theorem proving”. It is a rather broad term. I don’t think they added something much different than what they already had.
      2. IshKebab · 1789645670 · focus · HN ↗

         It is. Look up what SMT stands for.

         1. mcphage · 1789651339 · focus · HN ↗

            Shin Megami Tensei?
         2. NooneAtAll3 · 1789651849 · focus · HN ↗

            SMT is SAT+arithmetic, no?

            1. IshKebab · 1789658184 · focus · HN ↗

               Satisfiability Modulo Theories
      3. baq · 1789658234 · focus · HN ↗

         well a SAT solver is kinda sorta a theorem prover right...?
   3. okokwhatever · 1789659620 · focus · HN ↗

      nailed!
2. olooney · 1789652821 · focus · HN ↗

   I like Z3 a lot. I think it's criminally underappreciated and underused. Here is a fairly interesting use I put it to a few years ago:

   <a href="https:&#x2F;&#x2F;www.oranlooney.com&#x2F;post&#x2F;playfair&#x2F;#known-plaintext-attack" rel="nofollow">https:&#x2F;&#x2F;www.oranlooney.com&#x2F;post&#x2F;playfair&#x2F;#known-plaintext-at...

   Slightly more complicated than the toy examples shown in the documentation above, and hints at one of the real world use cases for Z3 - red teaming cryptography.

   That said, I&#x27;m not sure the documentation linked above is really doing it any favors in terms of helping popularizing it.

   1. lloydatkinson · 1789658919 · focus · HN ↗

      How does it compare to the others? I started trying to use Zinc but I get lost in all the vocabulary and literature which assumes you already have a background in it.

      1. Bluestein · 1789659555 · focus · HN ↗

         There&#x27;s also a neat shm library by that name. Namespace&#x27;s getting crowded :)
3. ascent817 · 1789663996 · focus · HN ↗

   I’m working on a DO-178C compliant verification suite for avionics software with Z3 at work, criminally underrated

Unofficial Hacker News client; not affiliated with Y Combinator.