Having fun with the revelation that Kagi Translate is actually something like a thin wrapper over an LLM, so you can pass anything you want as the "to" language in the URL's query string and it will do its best to "translate" your text to that

https://translate.kagi.com/?from=en&to=pentagon+speak&text=I+think+we+should+break+up.

I accidentally read LinkedIn again and lots of people are talking about the flow of writing code with an LLM and then using a feedback loop with formal verification to reject incorrect implementations.

On the surface, this seems sensible: LLMs can produce kind-of correct (or, at least, correct-looking) code rapidly, verification tools can tell you if it’s correct and you can just keep exploring the design space until you find something correct.

But the bit no one is talking about is: who writes the specification, which must be sufficiently detailed that it can reject incorrect things (including thins in the wrong complexity class, so you don’t accept when the LLM writes a factorial complexity algorithm where a linear one would work)? And why is writing a formal specification believed to be easier than writing code? And what tools can take an arbitrary program and prove that it does or does not implement a spec? If these things were all easy, formal verification would already be ubiquitous.

EDIT: I should say that I am a huge fan of formal verification and wish it were more common. I've worked with folks doing formal verification of a few things that I care about and my experience is that writing a good specification is a similar amount of effort to writing an implementation. Formally verifying equivalence between the specification and the implementation is much more work.

There's some work on LLMs + theorem provers to try to automate this, where you basically give the properties you want to prove and have it fill in the proof. The nice thing here is that the theorem prover will reject proofs that don't work (though you need to be careful that the LLM doesn't introduce new axioms or you end up with ex falso quodlibet issues [any property can be proven if you start with axioms that are false]). But that still requires a specification that captures everything that you care about in the program.

Thanks @stuartmarks for making me dig through some of #Naur's work

https://www.naur.com/comp/c8-1.html

> the idea that machines might be able to think appears to be […] dismaying to many people. It seems that the […] suggestion of such a possibility conjures up a nightmare of a machine-ridden world in which man […] is the slave of the machine. Such a fright your […] author finds groundless. He is worried that the danger lurks, not with the machines that perhaps can think, but with the people who cannot