I assume you're talking about Hoare logic, and yes, they still teach it in the more theoretical-CS-inclined departments and it's often at least given a mention in other programmes. In summary, Hoare logic gives you a way to prove the correctness of computer programs by writing what you know to be true at each stage of the execution of the program as a series of formal mathematical statements. Imagine you're some code to square a number, on the first line you might write something like "the variable x equals the number v, where v is the value that was passed to this program" and on the last line you might write "the variable x equals the number v * v". The goal of writing the proof is essentially to show logically how you get from one to the other by transforming that first statement into the last one.

Separation logic basically extends this framework by adding a collection of extra rules that allow you to 1. deal with concurrent programs that operate on a shared bit of information and 2. handle programs that use pointer-based data structures. This transforms Hoare logic from being a sorta clunky tool for theoreticians to something that can be used to verify programs in the Real World™ or at the very least detect bugs that aren't covered by syntactic (grammar) or simpler forms of semantic analysis (such as type systems - e.g. "do not let the user multiply the word 'hello' by 3"). In business scenarios, you wouldn't actually write these statements out by hand, but they would be used automatically by various software tools (basically bug-finders).

One of its inventors, Peter O'Hearn got head-hunted by Facebook, who now use it to statically detect bugs in their code. Also woah woah I just noticed they have developed an open-source application that uses it!!