From: "Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>
Subject: Ada principles outside of Ada
Date: Sun, 05 Aug 2012 23:32:27 +0200
Date: 2012-08-05T23:32:27+02:00 [thread overview]
Message-ID: <op.wik7gdttule2fv@douda-yannick> (raw)
Hi people,
Just for fun, two quotes from a captivating thesis about Isabelle, a proof
assistance and authoring environment, which has some words Ada users may
recognize as their own typical words.
In Markus Wenzel's 2001 thesis,
titled “Isabelle/Isar — a versatile environment for human-readable formal
proof documents”
http://tumb1.biblio.tu-muenchen.de/publ/diss/in/2002/wenzel.pdf
Page 18 (printed page 4)
“Here the primitive layer consists of abstract theorem
constructors of the inference kernel, according to
'Correctness by Construction' by Milner.”
Page 27 (printed page 13), talking about the Isar language design
rationals:
“Primacy of readability over writability.”
I may have a later question regarding Ada and SPARK and Isabelle.
--
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University
reply other threads:[~2012-08-05 21:32 UTC|newest]
Thread overview: [no followups] expand[flat|nested] mbox.gz Atom feed
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox