> You implement a formal spec for a requirement and/or high-level function that takes plaintext as input and outputs ciphertext. this misses the relationship b

> You implement a formal spec for a requirement and/or high-level function that takes plaintext as input and outputs ciphertext. this misses the relationship between the size of the plaintext and the ciphertext... edit: part of the problem is tooling, to deal with stuff like this you need dependent types and those do exist, but not in a way that "the programmer on the street" can use...