Comment by saithound

> Really unnecessary levels of snark here. [..] Have you ever heard of prolog?

Why do you look at the speck of sawdust in your brother's eye and pay no attention to the plank in your own?

> I’m sure a prolog program can express whatever property you’re attempting to write just as tersely

No, you won't be able to express the most basic properties in Prolog at all, let alone as tersely as in a proper specification language.

E.g. if you have a language interpreter and a bytecode interpreter, pretty much every specification language will let you express the correctness of a compiler `compile(x)` as

``` for all scripts x and inputs i,

bytecodeInterpreter(compile(x),i) == languageInterpreter(x,i) ```

Good luck expressing this in Prolog, let alone equally tersely.