Absolutely not, at least not to me. I'm not a huge type theory guy or anything.

But saying that "proofs are a burden especially for things with side effects like shooting a gun" when systems that shoot guns specifically do have proofs in spite of their type systems invalidates the example, if not the argument.

The presenters certainly think these languages will help construct those proofs.. that I'm less certain of.