it's kind of a proof assistant, not really a programming language, focusing on finding gaps in invariants during state transitions.

i suggest spending a few hours with author's own video course: https://lamport.azurewebsites.net/video/videos.html

it is generally useful, what it doesn't do is emit working prototypes.