3 ms·

Are there any reasons why searching Lisp word does not give any result? Possible reasons: its type system is uncrashable, its type system is as easy to crash as

Are there any reasons why searching Lisp word does not give any result? Possible reasons: its type system is uncrashable, its type system is as easy to crash as C program (I am too beginner to know which is true).

Jtsummers 3y ago
Probably for the same rationale they provided to exclude Python from examination: > Python's type system: Dynamic languages like Python do local type checks to establish global safety properties. However, the type checks are not done purely on the program's source code before running it, but examine the actual runtime inputs as well.
- shadowgovt 3y ago
  Interestingly, common lisp does allow one to write unsound programs intentionally. The `the` special operator (http://clhs.lisp.se/Body/s_the.htm#the http://clhs.lisp.se/Body/s_the.htm#the) declares that the form in the second position is of the type specified by the first position. You can imagine that this allows the runtime to crash early if the type is wrong, and you'd be right... But depending on the compiler you use, it also allows for the creation of unsound programs because you can set your flags such that the compiler uses the presence of `the` to make assumptions on the underlying types, letting the program evaluate faster by throwing out some runtime type checks.
  - tmtvl 3y ago
    Ah yes, good old (declaim (optimize (safety 0)))
  - kazinator 3y ago
    declarations are promises to the compiler. You're saying you've off-loaded all the heavy type checking and done a better job of it yourself, and your results should be used. So whether things are sound depends on your personal type system, and the sanitization of inputs to the whole thing so that your assumptions are met.
kazinator 3y ago
Lisps are excluded from that page because they (mostly) don't play the dangerous game that the page is about. The dangerous game is this: 1. Prove some things about the program graph. 2. Assume that your proof is correct, and translate the program accordingly (possibly with aggressive optimizations based on the proofs). 3. Remove all the proof artifacts from the program, such as types, and run the compiled code with no further safety net.* The entire Counterexamples project speaks to the truth in Donald Knuths' famous quote: "Beware of bugs in the above code; I have only proved it correct, not tried it." -- * Even if there is a safety net, the selling point of the languages is that it's unnecessary. If the type system is supposed to catch something, but it's not caught, and results in a run-time error (safely caught and everything) that still demonstrates unsoundness. It's not behaving as advertized/hyped.

Jtsummers 3y ago

Probably for the same rationale they provided to exclude Python from examination: > Python's type system: Dynamic languages like Python do local type checks to establish global safety properties. However, the type checks are not done purely on the program's source code before running it, but examine the actual runtime inputs as well.

shadowgovt 3y ago
Interestingly, common lisp does allow one to write unsound programs intentionally. The `the` special operator (http://clhs.lisp.se/Body/s_the.htm#the http://clhs.lisp.se/Body/s_the.htm#the) declares that the form in the second position is of the type specified by the first position. You can imagine that this allows the runtime to crash early if the type is wrong, and you'd be right... But depending on the compiler you use, it also allows for the creation of unsound programs because you can set your flags such that the compiler uses the presence of `the` to make assumptions on the underlying types, letting the program evaluate faster by throwing out some runtime type checks.
- tmtvl 3y ago
  Ah yes, good old (declaim (optimize (safety 0)))
- kazinator 3y ago
  declarations are promises to the compiler. You're saying you've off-loaded all the heavy type checking and done a better job of it yourself, and your results should be used. So whether things are sound depends on your personal type system, and the sanitization of inputs to the whole thing so that your assumptions are met.

kazinator 3y ago

Lisps are excluded from that page because they (mostly) don't play the dangerous game that the page is about. The dangerous game is this: 1. Prove some things about the program graph. 2. Assume that your proof is correct, and translate the program accordingly (possibly with aggressive optimizations based on the proofs). 3. Remove all the proof artifacts from the program, such as types, and run the compiled code with no further safety net.* The entire Counterexamples project speaks to the truth in Donald Knuths' famous quote: "Beware of bugs in the above code; I have only proved it correct, not tried it." -- * Even if there is a safety net, the selling point of the languages is that it's unnecessary. If the type system is supposed to catch something, but it's not caught, and results in a run-time error (safely caught and everything) that still demonstrates unsoundness. It's not behaving as advertized/hyped.