On Thu, Jan 26, 2012 at 3:24 PM, Nathan Rice <nathan.alexander.r...@gmail.com> wrote: > One of the nice things about Haskell is that the language is designed > in a way that is conducive to > proving things about your code. A side benefit of being able to prove > things about your code is that > in some cases you will be able to derive code just from well crafted > specifications (like higher order > Prolog). This isn't a game changer yet, but with advances in theorem > proving software and a thoughtful > language ontology, I could see it taking off very soon. Dijkstra was > focused primarily on this area for the > last 25 years of his life.
May I suggest a look at languages such as ATS and Epigram? They use types that constrain values specifically to prove things about your program. Haskell is a step, but as far as proving goes, it's less powerful than it could be. ATS allows you to, at compile-time, declare that isinstance(x, 0 <= Symbol() < len(L)) for some list L. So it might align well with your ideas. >> Probably deserves a better name than "constraintslib", that makes one >> think of constraint satisfaction. > > As you can probably tell from my other projects, I'm bad at coming up > with snappy names. I'm bad at doing research on previous projects ;) I'm sure another name will come up as the goals mature/solidify. -- Devin -- http://mail.python.org/mailman/listinfo/python-list
