3 ms·
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
by 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.