A blog about programming, theorem provers, and formal methods
Sorry that it’s been awhile since my last post! Big life stuff happening over here! Last time we designed a mechanism to accumulate stateful computation on Signals and Events. This design ended up looking a lot like a tiny version of the step-based reactive systems we designed in part 1, so some of you may have been wondering what the point of doing that is. We’ll answer that today: in this post…
Non-pointwise combinators have knowledge of previous timesteps Up to now, every Signal we’ve seen has been stateless. FRP . map and FRP . map2 from last time apply pure functions to the value at each timestep, with no memory of what came before. Real reactive systems have evolving state: the value at time t + 1 depends on the value at time t . In this post, we’ll build up to FRP . accumulate ,…
Last time, we introduced Signals, which are time-varying datatypes: at all time steps t , a Signal a produces some value of type a . We also saw that because an a is always available, the type of a Signal a is LTL.always a . So, we can write □ a to refer both to a a -producing Signal, as well as the universally-quantified temporal proposition. An Event occurs at some point in time The dual of a…
The Curry-Howard correspondence for LTL: FRP So far, what we’ve been doing is playing with LTL in the way that someone using a model checker like TLA+ might. We implemented a reactive system, executed some traces over that system, and wrote formulas to answer “does this trace satisfy this formula?” Later on, we saw how some formulas can be answered no matter which (valid!) trace is under…
In the previous posts, we saw how dependent types let us enforce that every step our reactive program took was valid, and how our monadic API gives us a nice way to sequence those steps (even if we lose static guarantees in the process). However, we hit the limits of what we could express in terms of propositions over our system’s traces. It’s straightforward enough to write statements about an…
Welcome back! Last time we implemented a simple reactive program in Lean. We implemented a pop machine State datatype, an Action type, and a step function that consumes a state, an action, and a logical proposition encoding why the action is valid for the given state, and produces a new state with that action applied. We also saw that while that step validity proposition was straightforward enough…
Over the holidays I spent a bunch of time seeing how far we could push Lean’s type system and built-in theorem prover to reason about everybody’s least-favourite interview problem . We actually had a lot to say about that, but Fizzbuzz is not exactly representative of most programs out there in the world: apart from the argument to the function, it doesn’t react to user input or other external…
A proof-carrying FB Last time we looked at the data definition of Vector a n , and saw that it was a structure type containing its runtime data (the backing Array a of elements) and a compile time-only proof relating the size of the array to n . One way to think about this data type is that every Vector instance carries that proof along with it (in practice, remember that owing to proof…
We started this series with a particular implementation of Fizzbuzz, and wrote our specification around that implementation. Having a tight coupling made it easy to relate the two, but a good specification is robust to different implementations of the same problem. It wouldn’t be good if there wasn’t a way to say, for example, “even though this implementation uses functional idioms and this other…
Welcome back! Last time, we got our dependently-typed fizzbuzz implementation to a point where we felt ready to prove our problem specifications: import Mathlib . Data . Nat . Basic -- implementation inductive FB : Type where | Fizz | Buzz | FizzBuzz | Num ( i : Nat ) instance : ToString FB where toString fb := match fb with | . Fizz => "Fizz" | . Buzz => "Buzz" | . FizzBuzz => "Fizzbuzz" | . Num…
In an earlier post, we learned a bunch of Lean’s syntax and saw how to write some simple theorems about the venerable(?) Fizzbuzz problem. In particular, we learned some simple tactics that can break down a theorem’s goal into simpler statements, until we are left with an axiomatically-true statement: The rw tactic lets us, if we have a proof of equality, substitute one side of the equality for…
Back in grad school, I ran a directed reading group for undergrads interested in the intersection of systems and PL research. Most weeks we just discussed papers, but the final session of the semester was special: I’d tell them, “Okay, all term you’ve seen what others have built; today, let’s write and verify some programs of our own!” So, we’d sit in a conference room with a text editor and a box…
This was work for a graduate seminar in model checking that I wrote with Sammy Thomas . I later adapted it into a Papers We Love NYC presentation. As it was written for a specialist audience, the prose is a lot denser than my ordinary style, but some of you may find it interesting anyway. Overview and Motivation Enterprising formal methods researchers could do worse than position their work in the…
This post originally appeared on Cohost . Last time we built up a mechanism to determine whether boolean sentences with equalities are satisifiable, without needing to “translate down” equalities into propositional logic. We saw that SMT solvers make use of two “translators”: one that encodes the theory down into propositional logic, and a theory-specific checker that deduces blocking lemmas for…
This post originally appeared on Cohost . So last time we introduced the notion of satisfiability theories that extend propositional logic to solve the satisfiability problem for more interesting logical sentences than those made up of booleans and logical connectives. We saw how formulas involving equality could be encoded by splitting on the two cases that make boolean equality true - both are…
This post originally appeared on Cohost . Previously , previously . Last time we built a basic conflict-driven clause learning (CDCL) solver that solves the boolean satisfiability problem. Recall that we started with a sentence in propositional logic containing boolean variables, and the solver told us whether there exists a satisfying assignment to those variables such that the whole boolean…
This post originally appeared on Cohost . Last time we talked about the Davis-Putnam algorithm for solving the Boolean satisfiablity problem (SAT). I think it would be fun to talk about how SAT can be used to reason about more interesting things than Boolean expressions, like linear arithmetic or array/pointer accesses. But before that, it probably makes sense to finish the actual SAT algorithm…
This post originally appeared on Cohost . The president has ordered all programmers to maximise their automated reasoning with these weird tricks! Logical agents hate this! Last night I was talking to a friend about how I should write more, and then only a few hours later I found myself wide awake at 2:30 AM, so what better time to get comfy and write a bit about something I find cool? If you’re a…
Welcome back to the final installment of Proving The Coding Interview! In the previous article we completed our verification of the venerable Fizzbuzz ( ) interview question by implementing a nat-to-string conversion function method . That helper was correct but suboptimal in terms of performance, and not really structured the way a developer would really implement it in an OOP language. Since…
Welcome back to Proving the Coding Interview! In the previous article we started to verify and implement an implementation of Fizzbuzz in the Dafny programming language. But we left off one important piece: Dafny doesn’t yet have built-in functionality to convert a number value to a string, which we need to complete Fizzbuzz ( ) 's behaviour. We’ll attempt to write such a conversion today and fix…
Enjoying programming interview questions is one of those things that nobody should admit to in polite company. But as with so many other things in life, a good gimmick can make the most tedious chore bearable if not outright pleasant. And if you’re a grad student and can use that chore as a procrastination tactic, then all the better! (Sorry, James , if you’re reading this, I’ll get on whatever it…
I use Ivy as part of my day-to-day research. It’s a cool language with lots of nice properties, but initially setting it up on a modern machine can be a bit tricky. It’s written in Python 2, which is no longer easily installable on modern systems, and requires a specific old version of Z3. As a result, it becomes tedious to juggle Python interpreter and dependency versions if you need Python and…