Version 1.0 released of Nim Programming Language

Offtopic
81

My understanding is that the key problem is that in general, proving something about types is difficult or infeasible, so for a large class of valid programs, even a very sophisticated compiler just can’t figure it out. Eg for

function fermat(a::Integer, b::Integer, c::Integer)
    # let's pretend there is no overflow
    if a > 0 && b > 0 && c > 0 && (a^3 + b^3 == c^3)
        "a fish"
    else
        42
    end
end

the result type is Int, but I am not sure very many compilers would figure this out (yes, this is a contrived example — but type inference can fail very easily in practice, too).

When this happens, traditionally “static” languages just consider your program invalid (not proven correct, it is considered incorrect). Instead, Julia will just try to work with it.

In general it is very difficult to prove that some code is incorrect in Julia in advance, because new methods, functions and global variables can be defined at any point between the definition and the AOT compilation.

4 Likes