Comment by PeCaN

11 years ago

We could have something similar with full dependent types a la Idris: you could write a proof and search for a function that satisfies it. If such a thing were popular and huge amounts of Idris code were written, you could write only proofs for your program and the Idris system could go download and piece together your program!

That would be very cool, but I'm not sure how much easier it would actually turn out to be. Also to do anything useful you'd probably have to restrict the language to be non-Turing-complete.

3 comments

PeCaN

Reply
andy9775  11 years ago

Similar idea but what if you were to write your tests first and then upload them to a site that pieces together the required modules to pass them and generates an API against the modules.

  • PeCaN  11 years ago

    Because finding code that passes arbitrary tests is undecidable in the general case.

    (Same reason the pseudo-Idris language would have to be non-Turing-complete)