Did they give you a formal semantics for the language in which you implemented algorithms? Or did you merely “prove” things about informal descriptions of algorithms?

No, proofs were usually done in an entirely separate class later, with the DSA classes focused on data structures (stacks, heaps, hash tables, etc.), sorting algorithms (merge sort, quicksort, etc.), and efficiency (e.g. using Big O). Such was the majority of the content in both cases, at least.

I still don't really have an answer to my question, though. What makes using a different language such a poor choice in this context?

> No, proofs were usually done in an entirely separate class later

Okay, now that is contemptible. And you didn't address my question: Were your proofs about actual programs, or merely about informal algorithm descriptions?

> What makes using a different language such a poor choice in this context?

The fact you would waste too much time teaching a second language at a sufficiently rigorous level to write proofs about programs written in it.