2 ms·

If we're trying to outline a future for assertions, I think it would help to situate them among the other mechanisms we have for ensuring correctness and explai

If we're trying to outline a future for assertions, I think it would help to situate them among the other mechanisms we have for ensuring correctness and explain where assertions have the right tradeoffs. For example, what unique need does a production assertion API satisfy that a normal conditional throw does not? Are there cases where production assertions are still necessary even when invariants are established through type constructors?

klibertp 2mo ago
Asserts are a goto of ensuring correctness. Versatile, powerful, and incredibly easy to misuse. Whatever correctness goal you're trying to achieve, there are safer, more ergonomic, and stronger alternatives you can reach for: type systems, contract systems, and even normal exception handling are often better. However, if you work in a domain where such tools can't be used or are not available, assert will still be there for you. It's worth knowing how to use it for that situation, but you should favor less ad hoc, more systematic features to ensure correctness in day-to-day programming.
rramadass 2mo ago
> For example, what unique need does a production assertion API satisfy that a normal conditional throw does not? See https://news.ycombinator.com/item?id=49231133 https://news.ycombinator.com/item?id=49231133 An "assert" is for "impossible to fail" conditions while "throw" is for conditions which might fail within the valid state space of the program. > Are there cases where production assertions are still necessary even when invariants are established through type constructors? Yes. Even though there is an equivalence between "Predicates <-> Types" (Curry-Howard correspondence) many languages do not have a robust type system to avail of this (eg. C). In the "Axiomatic" approach to "Programming Language Semantics" a language construct's (eg. if/switch/while etc.) specification is given by "precondition and postcondition" which are asserts that must hold before and after the construct. This is the famous "Hoare Triple" and later extended by Dijkstra in his wp-calculus and demonstrated in his "Guarded Command Language". The same idea holds when the code between precondition and postcondition is a function/class/module/etc. in which case it is called a "Contract" for that piece of code.

klibertp 2mo ago

Asserts are a goto of ensuring correctness. Versatile, powerful, and incredibly easy to misuse. Whatever correctness goal you're trying to achieve, there are safer, more ergonomic, and stronger alternatives you can reach for: type systems, contract systems, and even normal exception handling are often better. However, if you work in a domain where such tools can't be used or are not available, assert will still be there for you. It's worth knowing how to use it for that situation, but you should favor less ad hoc, more systematic features to ensure correctness in day-to-day programming.

rramadass 2mo ago

> For example, what unique need does a production assertion API satisfy that a normal conditional throw does not? See https://news.ycombinator.com/item?id=49231133 https://news.ycombinator.com/item?id=49231133 An "assert" is for "impossible to fail" conditions while "throw" is for conditions which might fail within the valid state space of the program. > Are there cases where production assertions are still necessary even when invariants are established through type constructors? Yes. Even though there is an equivalence between "Predicates <-> Types" (Curry-Howard correspondence) many languages do not have a robust type system to avail of this (eg. C). In the "Axiomatic" approach to "Programming Language Semantics" a language construct's (eg. if/switch/while etc.) specification is given by "precondition and postcondition" which are asserts that must hold before and after the construct. This is the famous "Hoare Triple" and later extended by Dijkstra in his wp-calculus and demonstrated in his "Guarded Command Language". The same idea holds when the code between precondition and postcondition is a function/class/module/etc. in which case it is called a "Contract" for that piece of code.