Curiously Empty Intersection of Proof Engineering and Computational Sciences
Kiiskinen, S. (2023). Curiously Empty Intersection of Proof Engineering and Computational Sciences. In P. Neittaanmäki, & M.-L. Rantalainen (Eds.), Impact of Scientific Computing on Science and Society (pp. 45-73). Springer. Computational Methods in Applied Sciences, 58. https://doi.org/10.1007/978-3-031-29082-4_3
Published in
Computational Methods in Applied SciencesAuthors
Date
2023Discipline
Computing, Information Technology and MathematicsLaskennallinen tiedeComputing, Information Technology and MathematicsComputational ScienceAccess restrictions
Embargoed until: 2025-07-08Request copy from author
Copyright
© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG
The tools and techniques of proof engineering have not yet been applied to the computational sciences. We try to explain why and investigate their potential to advance the field. More concretely, we formalize elementary group theory in an interactive theorem prover and discuss how the same technique could be applied to formalize general computational methods, such as discrete exterior calculus. We note that such formalizations could reveal interesting insights into the mathematical structure of the methods and help us implement them with stronger guarantees of correctness. We also postulate that working in this way could dramatically change the way we study and communicate computational sciences.
Publisher
SpringerParent publication ISBN
978-3-031-29081-7Is part of publication
Impact of Scientific Computing on Science and SocietyISSN Search the Publication Forum
1871-3033Keywords
Publication in research information system
https://converis.jyu.fi/converis/portal/detail/Publication/183921931
Metadata
Show full item recordCollections
License
Related items
Showing items with similar title or keywords.
-
Mutation testing in functional programming
Hopia, Tuomo (2023)In software engineering, mutation testing is a method to assess and improve software test quality. It is more prevalent in object-oriented programming and has only seen little interest in functional programming. In this ... -
Computational Rationality as a Theory of Interaction
Oulasvirta, Antti; Jokinen, Jussi P. P.; Howes, Andrew (ACM, 2022)How do people interact with computers? This fundamental question was asked by Card, Moran, and Newell in 1983 with a proposition to frame it as a question about human cognition – in other words, as a matter of how information ... -
Software Startup Practices : Software Development in Startups Through the Lens of the Essence Theory of Software Engineering
Kemell, Kai-Kristian; Ravaska, Ville; Nguyen-Duc, Anh; Abrahamsson, Pekka (Springer, 2020)Software startups continue to be important drivers of economy globally. As the initial investment required to found a new software company becomes smaller and smaller resulting from technological advances such as cloud ... -
Software patterns, organizational learning and software process improvement
Ahlgren, Riikka (University of Jyväskylä, 2011) -
Algorithms and Logic as Programming Primers
Niemelä, Pia; Valmari, Antti; Ali-Löytty, Simo (Springer Nature Switzerland AG, 2019)To adapt all-immersive digitalization, the Finnish National Curriculum 2014 (FNC-2014) ‘digi-jumps’ by integrating programming into elementary education. However, applying the change to mathematics teachers’ everyday praxis ...