$$\mathit{Total\ Correctness} = \mathit{Partial\ Correctness} + \mathit{Termination}$$
Program Verification
$$\mathit{Emacs} + \mathit{Go} = \mathit{Parametric\ Polymorphism}$$
Fulfilling a Pikedream: the ups of downs of porting 50k lines of C++ to Go.
$$\mathit{Product} = \mathit{Customer} \times \mathit{Business} \times \mathit{Technology}$$
What is a Product?
$$\mathit{Algorithm} = \mathit{Logic} + \mathit{Control}$$
Algorithm = Logic + Control
$$\mathit{Cost\ of\ Delay} = \mathit{User-Business\ Value} + \mathit{Time\ Criticality}\ + \mathit{Risk\ Reduction\ and}/\mathit{or\ Opportunity\ Enablement}$$
WSJF - Scaled Agile Framework
$$\mathit{Well}\ \text{-}\mathit{founded\ Semantics} + \mathit{Branch\ and\ Bound} = \mathit{Stable\ Models}$$
Well-founded Semantics + Branch and Bound = Stable Models
$$\mathit{Property\ Tests} + \mathit{Contracts} = \mathit{Integration\ Tests}$$
"Property Tests + Contracts = Integration Tests"
$$\mathit{Compiler}(\mathit{Program}) = \mathit{Algorithms} + \mathit{Data\ Structures}$$
Next-Paradigm Programming Languages (Wirth)
$$\mathit{Clingo} = \mathit{ASP} + \mathit{Control}$$
Clingo = ASP + Control : Preliminary Report
$$\mathit{Assets} = \mathit{Liabilities} + \mathit{Equity}$$
Balance Sheet - Definition & Examples
$$\mathit{Programming} = \mathit{Structure} + \mathit{Efficiency}$$
What is the use of Continuation Passing Style (CPS)?
$$\mathit{Screen} + \mathit{Camera} = \mathit{World}$$
How to use the SDL viewport properly?
$$\mathit{What} + \mathit{When} = \mathit{How}$$
The Timelines Approach to Consistency in Networked Games
$$\mathit{Successful\ Fiction\ Writing} = \mathit{Organizing} + \mathit{Creating} + \mathit{Marketing}$$
How To Write A Novel Using The Snowflake Method
$$\mathit{Model\ Theory} = \mathit{Universal\ Algebra} + \mathit{Logic} = \mathit{Algebraic\ Geometry} - \mathit{Fields}$$
Model theory - Wikipedia
$$\mathit{Demonic} + \mathit{Angelic\ Behaviour} = \mathit{Simulation\ Properties}$$
Deductive Verification with Ghost Monitors
$$\mathit{Dynamic\ Scope} + \mathit{Laziness} = \mathit{Counterfactuals}$$
Dynamic Scope + Laziness = Counterfactuals
$$\mathit{Safety} = \mathit{Progress} + \mathit{Preservation}$$
Types and Programming Languages, Section 8.3
$$\mathit{Money} \mathrel{+}= \mathit{Income} - \mathit{Spending}$$
Retire at 35
$$\mathit{Suffering} = \mathit{Pain} \times \mathit{Resistance}$$
Suffering = Pain x Resistance
$$\mathit{Separation\ Logic} + \mathit{Superposition\ Calculus} = \mathit{Heap\ Theorem\ Prover}$$
Separation Logic + Superposition Calculus = Heap Theorem Prover
$$\mathit{Constraint\ Program} = \mathit{Model} + \mathit{Search}$$
Constraint Programming
$$\mathit{Types} + \mathit{Values} = \mathit{Dependent\ Types} = \mathit{Types\ Refined\ with\ predicates\ over\ values}$$
Liquid Types
$$\mathit{Pitch\ Pipe} + \mathit{Piano} = \mathit{Pocket\ Pitch}$$
Pocket Pitch
$$\mathit{Refinement\ Types} = \mathit{Types} + \mathit{Logical\ Predicates}$$
Programming with Refinement Types
$$\mathit{Programming} = \mathit{Algorithms} + \mathit{Coding}$$
PlusCal Tutorial
$$\mathit{SAT} + \mathit{Theory\ Solvers} = \mathit{SMT}$$
First Order Logic (FOL) and Satisfiability Modulo Theories (SMT)
$$\mathit{GADTs} = \mathit{Algebraic\ Datatypes} + \mathit{Existential\ Types} + \mathit{Equality\ Constraints}$$
Polymorphic recursion in OCaml: return values
$$\mathit{Hoare\ triples} + \mathit{Monadic\ types} = \mathit{Hoare\ Type\ Theory}$$
Verification of Imperative Programs in Hoare Type Theory
$$\mathit{DSL\ design} = \mathit{Art} + \mathit{Lots\ of\ iterations}$$
FlashMeta: A Framework for Inductive Program Synthesis
$$\mathit{Inverse\ Semantics} + \mathit{Skolemization} = \mathit{Witness\ Function}$$
FlashMeta: A Framework for Inductive Program Synthesis
$$k\text{-}\mathit{FAIR} = k\text{-}\mathit{LIVENESS} + \mathit{FAIR}$$
Revisiting SAT-based Liveness Algorithms
$$\mathit{Cyclic\ proof} = \mathit{pre}\text{-}\mathit{proof}\ \mathcal{P} + \mathit{soundness\ condition}\ \mathcal{S}(\mathcal{P})$$
An introduction to cyclic proof
$$\mathit{coinduction} = \mathit{use\ of\ finality\ for\ coalgebras}$$
A Tutorial on (Co)Algebras and (Co)Induction
$$\mathit{Query} = \mathit{operation} + \mathit{pattern}$$
Adaptable Traces for Program Explanations
$$\mathit{word} + \mathit{word} = \mathit{compound\ word}$$
Why Chinese HATES 1 Syllable Words
$$\mathit{Consistency} = \mathit{joy}$$
The dev container CLI
$$\mathit{Genetic\ Algorithms} + \mathit{Neural\ Networks} = \mathit{Best\ of\ Both\ Worlds}$$
Genetic Algorithms + Neural Networks = Best of Both Worlds
$$\mathit{Profiling} = \mathit{Clustering} + \mathit{Synthesis}$$
Data-Driven Learning of Invariants and Specifications
$$\mathit{HOL} = \mathit{Functional\ Programming} + \mathit{Logic}$$
A Proof Assistant for Higher-Order Logic
$$\mathit{Lauschen} = \mathit{Hören} + \mathit{Fühlen}$$
Lauschen = Hören + Fühlen ... Wie Du dein eigenes Lied empfängst
$$\mathit{Code\ Review} = \mathit{Discussion} + \mathit{Code}$$
$$\mathit{Pull\ Requests} = \mathit{Compare\ View} + \mathit{Issue} + \mathit{Commit\ Comments}$$
Pull Requests 2.0
$$\mathit{ocamldebug} + \mathit{Time} = \mathit{max_int}$$
ocamldebug + Time = max_int
$$\mathit{Grokking} = \mathit{Phase\ Changes} + \mathit{Regularisation} + \mathit{Limited\ Data}$$
A Mechanistic Interpretability Analysis of Grokking
$$\mathit{Posterior\ probability} = \mathit{prior\ probability} + \mathit{new\ evidence}$$
Posterior Probability & the Posterior Distribution
$$\mathit{Static\ Analysis} + \mathit{LLM} = \mathit{AutoFix}$$
AutoFix
$$\mathit{Noninfluence} = \mathit{Noninterference} + \mathit{Nonleakage}$$
Information Flow Control Revisited: Noninfluence = Noninterference + Nonleakage
$$\mathit{Truffle} + \mathit{fries} = \mathit{Truffle\ fries}$$
Is GrabFood trialling AI generated pictures?
$$\mathit{MRDTs} = \mathit{Sequential\ data\ types} + \mathit{3-way\ merge}$$
Programming and proving distributed systems with persistent data structures
$$\mathit{backward\ compatibility} = \mathit{source\ compatibility} + \mathit{behavioral\ compatibility}$$
Proving Backward Compatibility for Object-Oriented Libraries
$$\mathit{SMT} = \mathit{SAT} + \mathit{expressiveness}$$
Quantifiers in Satisfiability Modulo Theories
$$\mathit{Prolog} = \mathit{Syntactic\ Unification} + \mathit{Backward\ Chaining} + \mathit{REPL}$$
How to implement a Prolog interpreter in a purely functional language?
$$\mathit{Go} + \mathit{Services} = \mathit{One\ Goliath\ Project}$$
Go + Services = One Goliath Project
$$\mathit{SelectML} = \mathit{OCaml} + \mathit{Select\ Query}$$
An SQL Frontend on top of OCaml for Data Analysis
$$\mathit{Tactile} + \mathit{Adaptive} = \mathit{Flux}$$
Flux
$$\mathit{360\ breathing} + \mathit{Kegel\ connection} = \mathit{The\ Foundation}$$
360 breathing + Kegel connection = The Foundation
$$\mathit{mutable\ state} + \mathit{lazy\ evaluation} = \mathit{death}$$
Why isn't lazy evaluation used everywhere?
$$\mathit{run} + \mathit{time} = \mathit{???}$$
"run" + "time" = ???
$$\mathit{SAT} = \mathit{ASP} + \mathit{Tertium\ non\ datur}$$
$$\mathit{ASP} = \mathit{SAT} + \mathit{Completion\ and\ loop\ Formulas}$$
From SAT to ASP and back!?
$$\mathit{ASP} = \mathit{KR} + \mathit{DDB} + \mathit{Search}$$
SAT and SMT for Answer Set Programming
$$\mathit{MOTIVE} + \mathit{MEANS} + \mathit{OPPORTUNITY} = \mathit{CRIME}$$
MOTIVE + MEANS + OPPORTUNITY = CRIME
$$\mathit{Coherence} = \mathit{Memoizing} + \mathit{Early\ Assumes}$$
Decidable Verification of Uninterpreted Programs
