Hacker News Reader

Comment by grogenaut | Hacker News Reader

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.

View on HN

Dependent 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).

What proof systems are you thinking about? Strong static types seem the most natural way to introduce formal verification into mainstream programming to me.

Well general mathmatecial proofs or TLA+... or would it be better to define "integer" as a strong type which I'm willing to concede.

I 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.

I guess that makes sense to count axioms as strongly typed.

(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.

Type checking can be represented as abstract interpretation. It is the mostly widely used kind of formal verification that exists.

Reply on news.ycombinator.com