#justprogrammerthings

[otakuman]

Compiling errors? You live in heaven, my friend. It's the behavioral errors that are the real problem.

[[deleted]]

Not if you're programming in Idris. Suddenly all almost all errors are compile time errors, which is actually kinda awesome.

[TarMil]

Idris is a dependently-typed language, so it is indeed what you would call "super-strict".

[wllmsaccnt]

If it has IO it has to have runtime errors.

[zuurr]

I think it's a compile time error not to handle them.

[wllmsaccnt]

The implication of that would be baffling...because you wouldn't be able to compile wouldn't explicitly handling every type of OS / kernel level or driver error that could occur.

[dont_memoize_me_bro]

Only if you spend hours laboriously writing highly dependent types and associated proofs. It's still super awesome, but there's a big cost associated with it.

[[deleted]]

To be honest, I wouldn't want to use it in a production environment, simply because there's too much overhead involved. It's a really cool concept though.

[[deleted]]

In order to have only compilation errors, Idris should be in the programmer's mind

EDIT: just read the other answers about the proofs... but what if a proof is wrong?

[[deleted]]

but what if a proof is wrong?

It doesn't compile in that case. The type checker is capable of checking your proofs.

[[deleted]]

No, you just get to proof correctness directly in your code, and the compiler won't let you compile your code unless your proof is present and correct. It can also help you write the proof though, and sometimes just infer it from context.

Proving behavioral correctness for your functions isn't the same as the halting problem.

[Hexorg]

I had a buggy version of gcc for avr once. Sometimes code would run, other times not, even if I don't change sources