Dijkstra on proof

That a proof is also the carrier of our understanding and that the joy of understanding is the last one we should delegate to machine is hardly stressed, probably because it cannot serve as a basis for funding.

AI does interpolations that I could have done myself

The current crop of AI image and video models washes a new class of videos ashore my Youtube recommendations: AI-enhanced historic footage. The 1920s, 1930s, etc. can now be watched in colour, high-definition and with clear sound. An artificial intelligence algorithm takes the original grainy black-and-white footage and interpolates what lies between the grains and below the film scratches. This is a fun party trick but it’s also utterly useless. The human brain already performs these interpolations and in most cases with less cliché and cringe. When I watch an original grainy recording of 1920s Berlin and then an AI-enhanced version thereof, I learn nothing new.

Formal core, natural language shell

A fundamental architecture pattern of functional software architecture is Functional Core, Imperative Shell. The gist of this pattern is that you design the core of your application (your domain logic, or: business logic) in a pure, immutable, algebraic (i.e. functional) language, and there's a surrounding shell that deals with the messy outside world of side effects and mutable state.

While working on an application that was mandated to include an "AI component" -- by which the sponsor of course meant: large language models --, I got the epiphany that LLMs only ever make sense as part of the user interface. This leads to a software design pattern similar to Functional Core, Imperative Shell, which I clunkily call ‘Formal Core, Natural Language Shell’.

The rationale behind Formal Core, Natural Language Shell is similar to the rationale behind Functional Core, Imperative Shell. In both cases, the former allows for clear, concise reasoning, which is vital for the application logic to work as intended. The latter is either a neccessity for which we have not yet found better abstractions (imperative shell) or a nice add-on that makes life easier (natural language shell).

In the case of the aforementioned software I built, which follows this pattern, the formal core consists of an RDF knowledge graph along with a simple modification logic based on git. The natural language shell allows users to specify a set of facts in English prose. An LLM then tries to translate this prose into RDF and presents a graphical representation thereof to the user. When the user confirms, the corresponding RDF data is committed to the formal core.