Over the last couple of weeks, I've been working on a personal project in Lean . Six months ago I would have used Clojure but the combination of Lean and AI assisted software engineering is making formal verification so easy, why wouldn't I choose the additional safety it brings? As part of this work, I needed a Markdown parser/renderer. The obvious route would be to wrap something like cmark-gfm…
A couple of weeks ago, I published Lean-ing into Software Engineering in which I hypothesized that the combination of the Lean Programming Language and AI-assisted coding meant that we were very close to the point where formal verification was realistic for everyday software engineering. Since then I've become convinced that we're not close: we're already there. In this article, I'm going to show…
The Lean programming language is revolutionising mathematics. More and more mathematical results have been formalised in Lean and it's increasingly becoming a standard part of the mathematician's toolbox. Lean didn't start out as a maths tool though; it was originally created to help with software verification: proving that software was correct. This is not a new idea: software verification was…
This follows on from my previous article which described how to get a simple Clojure Ring application running on AWS Lambda. This article shows how to connect it to a database. The accompanying code is here . CloudFormation AWS SAM provides direct support for DynamoDB, but not for more traditional databases like PostgreSQL, so that means dropping into CloudFormation. This is, sadly, rather wordy,…
I recently found myself starting a new project and was looking for the quickest and easiest way to get something up and running. In the past I might have used Heroku , and I looked briefly at Fly.io , but it turns out that Clojure now runs much better on Lambda than it used to (cold starts are no longer an issue), and it's easy to get up and running with AWS SAM which gives us simple serverless…
This is part 4 of a series. Part 1 | Part 2 | Part 3 | Part 4 The code to accompany this series is available here . In the previous part of this series, we saw how to use lattice semantics to calculate all our degrees of separation within the Game of Thrones dataset in one pass. But we didn't quite get to our final solution because we weren't yet calculating counts of the number of characters at…
This is part 3 of a series. Part 1 | Part 2 | Part 3 | Part 4 ] The code to accompany this series is available here . Harder, Better, Faster, Stronger It's very common that we want to find the "best" solution to a problem. Perhaps we want the shortest route between two points? Or the fastest? Or the most efficient? Or...? Flix's implementation of Datalog provides a feature known as "lattice…
This is part 2 of a series. Part 1 | Part 2 | Part 3 | Part 4 ] The code to accompany this series is available here . Injecting facts In part 1 of this series, we used Datalog rules to infer new facts about characters in Game of Thrones. But where do our initial facts come from? In part 1 we simply included them as part of our Datalog, but this isn't a scalable approach. We don't want to have to…
This is part 1 of a series. Part 1 | Part 2 | Part 3 | Part 4 The code to accompany this series is available here . Flix Flix is an exciting new programming language which provides the power of strongly typed functional programming with the accessibility of "programmer friendly" languages like Go, Rust, or Ruby. This article isn't about Flix, though, it's about Datalog, and the reason why Flix…