Similar to the experiences of other commenters, I find the LaTeX edit-compile-review cycle to only grow unreasonably slow when none of the incremental compilation features are used. For larger documents I recommend (i)…
SAT/SMT solving is indeed a much more structured approach and I agree that the analogy does not work too well for the backtracking part. I think that it rather applies to the well-established incorporation of "restarts"…
Datalog-ish query languages sure is a fun area to be working in. Such DSLs exist for various domains and, like Semmle's codeQL or the more academic Soufflé, Glean focuses on the domain of programming languages. Glean…
Here, "inverse" is an abbreviation of "multiplicative inverse" (aka. the reciprocal). Granted, shortening it to just "inverse" is misleading, but the name has stuck.
It is fun to read the source of old games for gems like the discussed `Q_rsqrt` function. However, one often wonders what the limits/assumptions/guarantees of such tricks are so I've blogged about SMT-based reasoning…
What a coincidence. I've also been looking into crossword generation recently. Have a look (https://bohlender.pro/blog/generating-crosswords-with-sat-sm...) if you're interested in a SAT-based solution. However, now…
While "soundness" and "completeness" are well-defined properties of deductive systems, using such formal methods for analysis of real-world systems requires their formalisation. However, the formalisation of any…
I didn't read it as a critique of formal program analysis either. In fact, several aspects of his approach can be found in formal verification of probabilistic systems. However to me, it seems that the author thinks to…
Application of formal methods is always an interesting read, and this article is a gentle introduction to some of the ideas exploited in probabilistic model checking. However to me, the way the article is written, gives…
Similar to the experiences of other commenters, I find the LaTeX edit-compile-review cycle to only grow unreasonably slow when none of the incremental compilation features are used. For larger documents I recommend (i)…
SAT/SMT solving is indeed a much more structured approach and I agree that the analogy does not work too well for the backtracking part. I think that it rather applies to the well-established incorporation of "restarts"…
Datalog-ish query languages sure is a fun area to be working in. Such DSLs exist for various domains and, like Semmle's codeQL or the more academic Soufflé, Glean focuses on the domain of programming languages. Glean…
Here, "inverse" is an abbreviation of "multiplicative inverse" (aka. the reciprocal). Granted, shortening it to just "inverse" is misleading, but the name has stuck.
It is fun to read the source of old games for gems like the discussed `Q_rsqrt` function. However, one often wonders what the limits/assumptions/guarantees of such tricks are so I've blogged about SMT-based reasoning…
What a coincidence. I've also been looking into crossword generation recently. Have a look (https://bohlender.pro/blog/generating-crosswords-with-sat-sm...) if you're interested in a SAT-based solution. However, now…
While "soundness" and "completeness" are well-defined properties of deductive systems, using such formal methods for analysis of real-world systems requires their formalisation. However, the formalisation of any…
I didn't read it as a critique of formal program analysis either. In fact, several aspects of his approach can be found in formal verification of probabilistic systems. However to me, it seems that the author thinks to…
Application of formal methods is always an interesting read, and this article is a gentle introduction to some of the ideas exploited in probabilistic model checking. However to me, the way the article is written, gives…