4 ms·
Which type system proves program correctness? A good type system can guarantee that your program doesn't suffer from certain classes of errors but that's very v
by MichaelSalib 13y ago
Which type system proves program correctness? A good type system can guarantee that your program doesn't suffer from certain classes of errors but that's very very far from correctness. Unless you only write programs that don't have any goal at all besides being memory safe: Behold MemSafe 2.9: it doesn't do anything at all, and most importantly, it doesn't do it in a memory safe way!
- DanWaterworth 13y agoAll safe type systems provide proofs that implementations fulfil specifications, but most type systems aren't expressive enough to create interesting specifications. The notable exceptions being type systems in dependently typed languages.
- gizmo686 13y agoA strong type system can do more than prove memory safety. It can guarantee that their are no unhandled cases, and that data has been properly processed before going into a certain use; however it (generally) cannot guarantee correctness. I say generally because the Haskell type system (with some extensions) is Turing complete, so you probably code implement a code prover in the type system.