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) splitting the document to leverage the \include and \includeonly commands, and (ii) using the Tikz library "external" to avoid the unnecessary recompilation of unchanged graphics. PGF/TikZ is often a bottleneck.
I agree though that it would be nice if the compilation (esp. from scratch) were generally faster.
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" of the search. Even thogh SAT/SMT solving is deterministic it still tries to avoid local maxima via such pseudo-random heuristics.
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 seems to still be work in progress, e.g. no support for recursive queries yet, but I wonder where they're heading. I'll certainly keep an eye on the project but I wonder how exactly Glean aims to -- or maybe it already does -- improve upon the alternatives? From the talk linked in another comment I guess the distinctive feature may be the planned integration with IDEs. Correct me if I'm wrong. Other contenders provide great querying technology but there is indeed no strong focus on making such tech really convenient and integrated yet.
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 about such properties using `Q_rsqrt` as an example: https://bohlender.pro/blog/smt-based-optimisation-of-fast-in... -- might be interesting to those not too familiar with the verification business.
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 I'll have to watch these videos for further insights.
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 real-world system will inherently introduce abstraction/assumptions. The question really is about which assumptions one should make when formalising software.
For example, when reasoning about software, one often abstracts from hardware details like battery-backed memory that will presist through a crash. There are also many "reasonable" assumptions at software-level, like `malloc` never failing, that many verifiers make in order to give more helpful results than "functional correctness is not guaranteed when using malloc".
The discussed paper is especially interesting for practitioners, as it tries to state all the assumptions made in the design of DR.CHECKER's static analysis. While this results in abstracting from certain realisable behaviours, e.g. "it treats each entry point independently" and misses state-dependent bugs, stating these assumptions helps with judging/estimating the quality of the results.
The paper's authors present a static analysis whose reasoning is sound w.r.t. stated assumptions. This is what they call "soundy". The actual post/article raises the important issue that it would be helpful to define what a sound static analysis of software is, that is agree on the assumptions/abstractions made.
However, picking a "reasonable" set of assumptions for a "sufficiently sound" static analysis is admittedly a difficult task, and of course not provided (yet).
It seems to me that finding a common set of assumptions is less of an issue for competitive software model checkers though, as the benchmarks used in the competition on software verification (SV-COMP) implicitly prescribe which aspects have to be modelled "properly". Couldn't a similar competition for static analysis give rise to a set of common assumptions for static analysis, too?
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 have accomplished the same thing as the author of TTTM.
> The mathematical method described here has a number of advantages over formal verification, including reduced code size and complexity.
My comment was intended to stress that the authors achieved different things. This article proved that the game design is sound, i.e. verification at model-level, while the original one proved that the implementation cannot reach certain undesired states. Both are perfectly reasonable, justifiable and necessary.
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 software verification, and CBMC in particular, an unnecessary bad reputation.
> There is no need to define “game progress” or implement a naive game AI, as formal verification methods appear to require.
> The mathematical verification code is about one-third the size of the formal verification code presented by the TTTM author
Most of the author's argumentation stems from the different levels of modelling. He pursues verification at model-level. That is, he does the interpretation that a "game progress"/"native game AI" would provide, and lifts the problem from the source-level to a formal representation as Markov process.
With that in mind, it should be clear that reasoning on that higher level can be done more efficiently. In fact, if the author of TTTM would have chosen to verify just the transition relation, an even simpler modelling would have sufficed, e.g. via Prism, ITSTools/GAL, SMV.
I just want to stress that the author of TTTM did not just formally verify that the concrete transition relation can not reach a "bad state", but proved that the actual implementation indeed cannot reach said states. For example, this also includes proving that the game's pseudo-random generation of initial states is safe to use.
> The TTTM formal verification code requires a value called MAX_FINISH_DEPTH, which represents the maximum number of steps required to finish the game from any valid state. It is unclear how the TTTM author arrived at the number 18, but the value can easily be calculated using the matrix representation of the game.
Again, when reasoning at the level of an actual implementation, i.e. software/binaries, such high-level reasoning is not applicable. Therefore, when employing bounded verification techniques, an educated guess about a sufficiently high number of steps must be provided.
I agree though that it would be nice if the compilation (esp. from scratch) were generally faster.