[typish]

Also interesting is their F* language: http://fstar-lang.org/

"F* is a new higher order, effectful programming language (like ML) designed with program verification in mind. Its type system is based on a core that resembles System Fω (hence the name), but is extended with dependent types, refined monadic effects, refinement types, and higher kinds. Together, these features allow expressing precise and compact specifications for programs, including functional correctness properties. The F* type-checker aims to prove that programs meet their specifications using an automated theorem prover (usually Z3) behind the scenes to discharge proof obligations. Programs written in F* can be translated to OCaml, F#, or JavaScript for execution. "

It's open source too: https://github.com/FStarLang/FStar

[nutate]

Gotta love automatic theorem proving. I read the Shen language book on "logic, proof and computation" which got me into the idea of a theorem prover inside of your normal language.

[zaszrespawned]

I'm going to write a package manager and call it F* ck

[SideburnsOfDoom]

There's already a mocking lib called Foq: http://trelford.com/blog/post/fstestlang.aspx

[runT1ME]

Have you worked with it? I love the idea of a fully powered F# without the kiddie gloves. F* looks pretty neat.