4 ms·
I'm not sure static typing is tied to formal verification. In fact if you think about it most proofs are basically typeless I a lot of cases.
by grogenaut 9y ago
I'm not sure static typing is tied to formal verification. In fact if you think about it most proofs are basically typeless I a lot of cases.
- seanwilson 9y agoWhat proof systems are you thinking about? Strong static types seem the most natural way to introduce formal verification into mainstream programming to me.
- grogenaut 9y agoWell 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.
- tom_mellior 9y ago(Not the parent here.) ACL2 is a prominent example of a proof assistant without a strong static type system; its object language is a pure subset of Common Lisp. The lack of static types is one of the reasons I find proving in ACL2 to be painful, but others have done amazing stuff with it.
- Cybiote 9y agoDependent or even refinement type systems are where a great deal of research into proof carrying code is done (for refinement types, since systems are restricted to decidability, the proofs are automatic but more limited).
- UncleMeat 9y agoType checking can be represented as abstract interpretation. It is the mostly widely used kind of formal verification that exists.