> You can’t prove even very simple universal properties of dynamically typed code, such as “when given an integer, this function always returns an integer” Rea

> You can’t prove even very simple universal properties of dynamically typed code, such as “when given an integer, this function always returns an integer” Really? Straight from my common lisp (SBCL) command line: CL-USER> (defun myfunction (x) (atanh x)) MYFUNCTION CL-USER> (describe #'myfunction) #<FUNCTION MYFUNCTION> [compiled function] Lambda-list: (X) Derived type: (FUNCTION (T) (VALUES (OR (SINGLE-FLOAT -1.0 1.0) (DOUBLE-FLOAT -1.0d0 1.0d0) (COMPLEX SINGLE-FLOAT) (COMPLEX DOUBLE-FLOAT)) &OPTIONAL)) Source form: (SB-INT:NAMED-LAMBDA MYFUNCTION (X) (BLOCK MYFUNCTION (ATANH X))) ; No value CL-USER> What happened here? I defined a function, i never declared which type does the function use, but the compiler can infer all the types. If i supply a string to "myfunction", the compiler will complain. Typing is strong, but it's dynamic. What will atanh return? CL-USER> (describe #'atanh) #<FUNCTION ATANH> [compiled function] Lambda-list: (NUMBER) Declared type: (FUNCTION (NUMBER) (VALUES (OR SINGLE-FLOAT DOUBLE-FLOAT (COMPLEX SINGLE-FLOAT) (COMPLEX DOUBLE-FLOAT)) &OPTIONAL)) Derived type: (FUNCTION (T) *) Documentation: Return the hyperbolic arc tangent of NUMBER. Known attributes: foldable, flushable, unsafely-flushable, movable, recursive Source file: SYS:SRC;CODE;IRRAT.LISP ; No value CL-USER> The wonders of CL... not only i get all the possible input types, but also the return types. And the documentation, and the source code file(!)