Timeline for Implementing Tarjan's strongly connected components algorithm in a language without exceptions or undefined behavior
Current License: CC BY-SA 4.0
4 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 26, 2019 at 4:26 | comment | added | isekaijin | @ApiwatChantawibul: In formal logic, there are results like “formal system S is not strong enough to prove theorem T”. Results like “type system S cannot verify invariant T” should be completely analogous. (Note, however, that I do not want to verify everything about Tarjan's SCC algorithm. I want to verify just enough to elide the redundant nonemptiness check.) | |
| Oct 26, 2019 at 0:42 | comment | added | Apiwat Chantawibul | I'm wondering about this myself. There is probably a formal proof out there along the lines of "We could let compiler check any (propositions/types) at compile time, but that would make type-checker turing complete". | |
| Oct 25, 2019 at 17:17 | comment | added | isekaijin | This is a perfectly fine engineering answer. But, as a mathematician, I'd like to determine formally the limits of the type system's expressive power. So I want a proof that this invariant is inexpressible in a conventional type system, like Java's or ML's or Haskell's. Unfortunately, as a rather traditional mathematician, I'm not proficient enough in type theory to carry out the proof myself, so perhaps a computer scientist could help me? | |
| Oct 25, 2019 at 17:07 | history | answered | D.W.♦ | CC BY-SA 4.0 |