In this talk I will introduce behavioral logics, esp. hidden logic and hidden algebra. Circular coinduction and the proof tool BOBJ that implements circular rewriting of order sorted hidden logic will be presented. Weak behavioral semantics is introduced and motivated as appropriate for software development using algebraic techniques. A specification of constraint automata in hidden logic closes the talk.