Those can be integrated with dependent types too - for an example look at F*.