3 ms·
> Compiling does not prove correctness for any program inputs. It can. For example in Scala there are libraries that allow you to define types for inputs e.g.
by threeseed 3y ago
> Compiling does not prove correctness for any program inputs.
It can.
For example in Scala there are libraries that allow you to define types for inputs e.g. this Int must be non-negative or this String must be greater than 5 characters.
https://github.com/fthomas/refined https://github.com/fthomas/refined
- westurner 3y agoAre those (non-Enum) precondition value constraints checked at compile-time or at runtime?
- threeseed 3y agoCompile time. But obviously only for values that are determined within the code.
- westurner 3y agoWhat does Rust do at runtime if you pass a non-const to a const field at a low level at runtime? If there's no runtime type or and value constraint checking, IMHO it shouldn't be considered proven at all. IIUC e.g. NASA's guidelines specify hard preconditions at the top of every function.
- westurner 3y agoFWIW, in Python, from https://news.ycombinator.com/item?id=38579378 https://news.ycombinator.com/item?id=38579378 : > Hypothesis generates tests from type annotations; and icontract and pycontracts do runtime type checking. Pynguin also generates tests; but it does not use icontract-style type and value constraints as decorator preconditions in generating tests. icontract-hypothesis: https://github.com/mristin/icontract-hypothesis https://github.com/mristin/icontract-hypothesis https://news.ycombinator.com/item?id=38138319 https://news.ycombinator.com/item?id=38138319
- Ferret7446 3y agoNo it doesn't. How would compiling prove this is wrong? # pseudocode def main(): a, b = argv[:] print(add(a, b)) def add(a, b): return a * b