I think the thing is that you write code in dynamic languages that you would never think to write in typed languages because it's just too against the culture/g

I think the thing is that you write code in dynamic languages that you would never think to write in typed languages because it's just too against the culture/grain. Two common situations in my job of throwing data around: Dataframes and pivoting- here the type of a thing (its columns) is never going to be easily statically provable because operations modify it dynamically. Reactive/dataflow style programming- look at the python MDF library, you annotate functions and it dynamically infers a dataflow graph from your code. You can do dataflow in typed languages but nowhere near as elegantly normally. These two things are core to what I do and drive a train through a typesystem. I think that the best possible solution would be to have some way to embed proofs and individual typesystems in different parts of your program, like a dynamic language with plugged proofs and types not a single typesystem language that you sometimes go around or switch off.