Re:Make CPython segfault in 5 lines of code
by dependenttypes on Friday December 20, 2019 @10:13AM
(#21844724)
You can trivially prove bottom in Haskell. Something like Agda or Idris would indeed fit the bill better.
Anyway, I said that this specific issue would not occur in a language with dependent types -- where incorrect code would cause the implementation to crash. Not that it is impossible to have a buggy compiler that at certain cases produces segfaults.
Re:Make CPython segfault in 5 lines of code
by shakna on Friday December 20, 2019 @03:54PM
(#21847309)
> Not that it is impossible to have a buggy compiler that at certain cases produces segfaults.
That's exactly what happened here, however. The instance check was missing from the interpreter.
Dependant types wouldn't have solved the underlying problem.
At a guess, you want something with dependent types?
Like Idris, or Haskell. You already have a Haskell example. This [0] release of Idris fixed a segfault when concatenating strings.
Maybe you meant a language that is proven from the ground up. Like CakeML. You can find a segfault example here [1].
Maybe you meant a language with an algebraic type system like Ada. You can find a segfault example here [2].
Maybe you meant something like Dotty (Research for the next version of Scala). You can find a segfault example here [3].
In short: You'll need to describe what you believe to be a "proper" type system, and name the languages you think fit that description, or no one can have a conversation with you.
[0] https://www.idris-lang.org/idris-1-1-1-released/
[1] https://github.com/CakeML/cakeml/issues/438
[2] https://stackoverflow.com/questions/56227629/segmentation-fa...
[3] https://github.com/lampepfl/dotty/pull/7466/