In recent years we have explored using Haskell alongside a traditional mathematical formalism in our large-enrolment university course on topics including logic and formal languages, aiming to offer our students a programming perspective on these mathematical topics. We have found it possible to offer almost all formative and summative assessment through an interactive learning platform, using Haskell as a lingua franca for digital exercises across our broad syllabus. One of the hardest exercises to convert into this format are traditional written proofs conveying constructive arguments. In this paper we reflect on the digitisation of this kind of exercise. We share many examples of Haskell exercises designed to target similar skills to written proof exercises across topics in propositional logic and formal languages, discussing various aspects of the design of such exercises. We also catalogue a sample of student responses to such exercises. This discussion contributes to our broader exploration of programming problems as a flexible digital medium for learning and assessment.
翻译:近年来,我们探索了利用Haskell和传统数学形式主义一起使用哈斯凯尔(Haskell)和我们大型大学课程中包括逻辑和正式语言在内的传统数学形式主义,目的是向我们的学生提供关于这些数学主题的编程观点,我们发现有可能通过互动学习平台提供几乎所有的成形和总结性评估,利用哈斯凯尔(Haskell)作为我们广泛教学大纲中数字练习的一种语言,最难转换成这种形式的练习之一是传统的书面证据,传达建设性的论点。我们在本文件中思考了这种练习的数字化。我们分享了许多哈斯凯尔练习的例子,这些练习旨在将类似技能作为在代言逻辑和正式语言中进行的书面证明练习的目标,讨论这种练习的设计的各个方面。我们还将学生对此类练习的反应编成样本。这种讨论有助于我们更广泛地探讨作为学习和评估的灵活数字媒介的编程问题。