Jump to content

Talk:Extended static checking

Page contents not supported in other languages.
From Wikipedia, the free encyclopedia

"ESC can identify a range of errors which are currently outside the scope of a type checker, including division by zero, array out of bounds, integer overflow and null dereferences."

This is not strictly true. With subtypes and refinement types all of these are "catchable" by a type checker. See for example http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2013/01/01/refinement-types-101.lhs/ Which is a tutorial on refinement types to remove division by zero. Languages like ATS use dependent types to prove the absence of errors like null dereferences. Integer over(under)flow and array out of bounds can be removed with subtypes, as done in CCured.

Start a discussion about improving the Extended static checking page

Start a discussion