Ada SPARK is better than languages with dependent types because it's actually used by the real word, not only by a team of circlejerking fat low iq niggers.
The Z3 theorem prover from Microsoft Research is now on Github, and more importantly now released under the MIT license. This is a true open source license allowing commercial use, unlike the previous non-commercial use only license. It's been used with LLVM in the ALIVe project. Work has already begun to integrate it directly into LLVM.
Name:
Anonymous2015-04-07 13:04
>>3 He who would trade GNU/Freedom for some perceived security, deserves neither GNU/Freedom nor security.
true open source license allowing commercial use, unlike the previous non-commercial use only license
Who would even care about the license on open-source code? Just steal it, merge it into your closed-source proprietary product, and no one's going to know. You only have to follow licenses when you open source.