Dependant types vs operational semantic

[Yannick Duchêne]

These past few days, I though it would be useful I plan to have some experiment with logic, in an unknown future, since I don’t have time now.

I was quickly reading things about logic as it happens, when I had this question: is there more or less expressiveness with dependant types and operational semantic? Is one more expressive than the other?

Dependant types is about type as proof, but I feel to understand not dependant types can carry proof, in operational semantic, that’s how this question came to me.

Or may be both are closely related?

Providing I understand things correctly …