* Ada principles outside of Ada
@ 2012-08-05 21:32 Yannick Duchêne (Hibou57)
0 siblings, 0 replies; only message in thread
From: Yannick Duchêne (Hibou57) @ 2012-08-05 21:32 UTC (permalink / 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
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2012-08-05 21:32 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2012-08-05 21:32 Ada principles outside of Ada Yannick Duchêne (Hibou57)
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox