Reading Paulson!! Right ON!! lol
[quote] ML also permits symbolic names. These consist of the characters ! % & $ # + - * / : < = > ? @ \ ˜ ‘ ˆ |
Names made up of these characters can be as long as you like: ----> $ˆ$ˆ$ˆ$ !!?@**??!! :-|==>-># Certain strings of special characters are reserved for ML’s syntax and should not be used as symbolic names: : | = => -> # :>
A symbolic name is allowed wherever an alphabetic name is: val +-+-+ = 1415; > val +-+-+ = 1415 : int [/quote]
What purpose would this cryptic-tude serve? Obfuscation? Seeding brain cancer? What? Or do most of you simply ignore this allowance?
Enjoying Paulson!! And so far, Poly&Paulson are a team!! :)
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
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
-
Duke Normandin -
Makarius