On Wed, 21 Jan 2026 15:53:00 +0100 Makarius makarius@sketis.net wrote:
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.
Thank you! However, I'm certain that Isabelle and I would not hit it off on our first date, as I am dumb-as-a-rock with regards to mathematics higher than algebra.
Neither do I play nice with .NET/Windows - so F# is out. OCAML seems too big and heavy for my liking.
I'm hoping that I can use Poly/ML simply as a general-purpose language so that I can try my hand with functional programming outside of a Lisp environment.
Thx again for the heads-up about darling Isabelle! LOL