Available under Creative Commons-ShareAlike 4.0 International License. Download for free at http://cnx.org/contents/383d4b87-2d7b-454e-99fe-2eaa43eae8ff@20.20
Recall examples of where we'd like proofs:
- WaterWorld (Is a certain location guaranteed safe?)
- type checking (Does a program call functions in the proper way?)
- circuit verifcation (Does a circuit always work as advertised?)
After seeing the reasons why proofs are important, we ended with a call for first needing a precise language for writing down statements without the ambiguity of English.
ASIDE: Might a programming language be a good way to specify formal concepts without ambiguity? Programming languages are usually motivated by speciflying how to do something (implementation), rather than formally speciflying what is being done (interface). While there is a deep relation between these two, logic is more appropriate for speci flying the "what".
- 1374 reads
