4 ms·

This is just Idris propaganda.

• abstractbeliefs 11y ago
  So what if it is, if Idris is a useful tool for the task? Seems a bit of a non-comment.
  • fiatjaf 11y ago
    Not at problem at all. I am even looking at Idris right now and I haven't never heard of it before.
• js8 11y ago
  Maybe that's where the things in programming are going? I think eventually we (programmers) end up with some hybrid system, where lot of stuff that's normally done by hand (refactoring, data transformations, dependency injection, data structure choice, optimization for speed and memory usage, parallelization, deduplication, unit testing) will be done by some theorem prover, working alongside the programmer.
  • incepted 11y ago
    > Maybe that's where the things in programming are going? Doubtful. Idris is probably the most visible current effort in that direction and even it is extremely obscure and barely known beyond the Haskell afficionado circles. And for good reasons: even today, Idris can barely express any program more complicated than the simplest mathematical formulas. Developers need languages that help them express network requests and database queries safely and efficiently, and Idris (and dependent languages in general) are not remotely close to being able to express that.
• kpmah 11y ago
  (author here) I don't even use Idris! I learnt it a couple of days ago for the purpose of this article. If Idris looks good it's not my fault :)
• orblivion 11y ago
  Coming from the powerful Idris lobby!