| If you are speaking about execution speed, you got the idea wrong. From a quote in the article: > If you use the high level typing stuff coding is a lot more work and requires more thinking, [...] (but) you can even hope for better performance than C by elision of run time checks otherwise considered mandatory, due to proof of correctness from the type system. Expect over 50% of your code to be such proofs in critical software and probably 90% of your brain power to go into constructing them rather than just implementing the algorithm. It's a paradigm shift. The idea is to formally prove that the code is not doing unexpected things. The process is relatively simple to understand: First you define the assumptions you make about the program, its execution environment, and the acceptable/expected results of your program. This is known as "formal specification" of the program. It is a critical part. If your specification is wrong, then the whole approach breaks down. However, this part should be much smaller than your whole codebase, and hence you can be extra careful on it. Next, using this specification, you write proofs showing that the code can not do anything unintended (such as accessing a buffer out of its valid range). The compiler goes through this proofs and checks that everything is provably correct (according to the specification). Then it can generate code without runtime checks that you would otherwise probably implement, because it is sure that certain things cannot happen. As a result, the code may end up being actually faster. Although a bit involved, the idea should be pretty intuitive. It is exactly what you are doing in your mind when programming. The main differences are: 1. We humans are pretty comfortable working with inexact and/or incomplete specifications. Then some undefined behavior happens, and our programs bug out. For instance, it is very easy for us to think about the division operator as something that always yields a value, ignoring the "division by zero" edge case. Computers are not, and force you to specify what exactly should happen when you encounter such edge cases. 2. We are also pretty bad at exhaustively checking every possibility, whereas computers excel at it. With the help of human-written proofs, obviously (otherwise verifying a program would involve checking every possible input for it, which is obviously intractable). TL;DR: The tradeoff here is between development and compilation speed versus correctness, which implies improved security and execution speed. |