6 ms·
Well general mathmatecial proofs or TLA+... or would it be better to define "integer" as a strong type which I'm willing to concede.
by grogenaut 9y ago
Well general mathmatecial proofs or TLA+... or would it be better to define "integer" as a strong type which I'm willing to concede.
- seanwilson 9y agoI don't feel there's much difference between e.g. the Coq way where types are used to bake specifications + proofs into the program and the Isabelle way where you write a program with less complex types and prove properties about the program after the fact. General mathematical proofs? If you mean paper proofs they wouldn't be considered formal as they don't go down to the axiom level.
- grogenaut 9y agoI guess that makes sense to count axioms as strongly typed.