This talk will focus on one such verification approach that takes as input a design under verification (DUV), modest architect-friendly DUV metadata, and a HW-SW contract. The approach automatically generates many simple formal properties that provably compose to imply the contract, and then evaluates them against the DUV to assess contract compliance. The enabling insight is that many important HW-SW contracts decompose into instantiations of a small, finite set of property templates, fillable automatically from the supplied metadata or from the results of evaluating other generated properties. This verification approach eliminates manual property writing, targets full HW-SW contracts rather than coverage metrics, and yields properties simple enough that commercial formal model checkers can produce unbounded proofs for most, even on complex designs.

One consequence of this is that checking whether assumptions hold is a different problem from verifying that your code works given the assumptions. Like to make sure “all unsafe blocks are safe” can’t use the Rust compiler, you need a second tool like Miri. I wonder if checking assumptions is, in practice, generally more difficult than checking everything else.

A formal type of proof most frequently encountered in elementary geometry courses in which known or derived statements are written in the left column, and the reason that each statement is known or valid is written next to it in the right column. The proof then proceeds from the known facts to the theorem to be demonstrated. […] However, this form of proof is virtually never used by practicing mathematicians because its confining and verbose format render it of very limited utility to any but the most simple of theorems.

Hmm, maybe this is why people don’t like Lean LOL.

Horn clauses are a Turing-complete subset of predicate logic. Horn clauses are the logical foundation of Prolog.

see: https://www.metalevel.at/prolog/logic

A topic first heavily covered in my learning by Wadler, now reintroduced to by by Baez. Happy to see it has a name.

via: https://www.youtube.com/watch?v=DAGJw7YBy8E

Curry is a declarative multi-paradigm programming language which combines in a seamless way features from functional programming (nested expressions, higher-order functions, strong typing, lazy evaluation) and logic programming (non-determinism, built-in search, free variables, partial data structures). Compared to the single programming paradigms, Curry provides additional features, like optimal evaluation for logic-oriented computations and flexible, non-deterministic pattern matching with user-defined functions.

via: https://buttondown.com/hillelwayne/archive/the-angels-and-demons-of-nondeterminism/

Do we care about the best case or the worst case?

How we can think about pushouts as applying rules via substitution, featuring examples in categorical databases and Datalog.

Today we’re excited to announce the first pre-alpha release of our new software CatColab 0.1: Hummingbird. CatColab is software for making models of the world together.