From c12ce5c3d942e76fe4d45a41912da48544a67316 Mon Sep 17 00:00:00 2001 From: wadler Date: Tue, 17 Apr 2018 19:28:17 -0300 Subject: [PATCH] started to write Modules and Collections --- src/Preface.lagda | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/src/Preface.lagda b/src/Preface.lagda index c29809d7..d82809a8 100644 --- a/src/Preface.lagda +++ b/src/Preface.lagda @@ -28,12 +28,11 @@ an excellent time to comment on the first part. Since 2013, I have taught a course on Types and Semantics for Programming Languages to fourth-year undergraduates and masters students at the University of Edinburgh. That course is not based on -the excellent [Types and Programming Languages][tapl] by Benjamin -Pierce, but on Pierce's subsequent textbook, [Software Foundations][sf], -written in collaboration with others and based on Coq. I am convinced -of Pierce's claim that basing a course around a proof assistant aids -learning, as summarised in his ICFP Keynote, [Lambda, The Ultimate -TA][ta]. +Benjamin Pierce's excellent [TAPL][tapl], but on Pierce's subsequent +textbook, [Software Foundations][sf], written in collaboration with +others and based on Coq. I am convinced of Pierce's claim that basing +a course around a proof assistant aids learning, as summarised in his +ICFP Keynote, [Lambda, The Ultimate TA][ta]. However, after five years of experience, I have come to the conclusion that Coq may not be the best vehicle. Too much of the course needs to