On Thu, Jun 4, 2015 at 9:10 AM, Jonathan S. Shapiro <s...@eros-os.org> wrote: > On Wed, Jun 3, 2015 at 8:11 PM, Matt Oliveri <atma...@gmail.com> wrote: >> >> On Wed, Jun 3, 2015 at 10:17 AM, Jonathan S. Shapiro <s...@eros-os.org> >> wrote: > > >> >> > I think there is a human factors tradeoff. "Weak" type systems are weak >> > in >> > the sense that they say much less about guarantees, but "strong" in the >> > sense that the humans actually understand what the stated guarantees >> > *are*. >> > Guarantees that I can't understand don't provide me with a lot of value. >> >> That's true, I guess. But _someone_ understands them, right? Or else >> how did they get there? > > > Sadly, there is a lot of reason to think that specification errors are > extremely common. Largely because the people writing the specifications > often *don't* understand them. > > Peter Gutmann has written a lot about this.
FWIW, theres some papers that have been done on defects in the SML definition, the following with the goal to list them all, http://www.mpi-sws.org/~rossberg/papers/Rossberg%20-%20Defects%20in%20the%20Revised%20Definition%20of%20Standard%20ML%20%5B2013-09-18%20Update%5D.pdf interestingly it contains something recently discussed as a [major] defect which is the 'and' keyword for mutually recursive types... _______________________________________________ bitc-dev mailing list bitc-dev@coyotos.org http://www.coyotos.org/mailman/listinfo/bitc-dev
