On 21/01/2026 15:38, Duke Normandin wrote:
Enjoying Paulson!! And so far, Poly&Paulson are a team!! :)
Indeed. The reason: Larry Paulson was building his Isabelle proof assistant approx. 1985 while David Matthews was working on Poly/ML.
Many decades later, Isabelle provides its own version of ML, based on Poly/ML, but quite different in style and manner. There is also a full-scale IDE around it. The idea is to edit proofs and programs in a stateless manner, as a structured document. The document is partially checked / evaluated, while you continue editing. No command-line anymore, no REPL (read-eval-print loop).
See https://isabelle.in.tum.de for the current release, with downloads for Linux, Windows, macOS. The Isabelle/jEdit Prover IDE has a Documentation panel, with src/HOL/Examples/ML.thy for regular Isabelle/ML, and Tools/SML/Examples.thy
Further below in the Documentation panel, there is a PDF document "implementation", which is about Isabelle/ML used to implement the prover engine. We don't have a proper introduction to Isabelle/ML. The Paulson book may serve as a starting point, but it is a bit old and dated in many respects.
Trigger warning: All of this might cause a severe cultural shock, compared to what you have heard about Standard ML (or other similar languages) so far.
Makarius