Smart contract programming languages represent a critical frontier in blockchain technology, demanding rigorous analysis of language design, security features, and runtime semantics. This survey presents a systematic examination of programming languages used for smart contract development across major blockchain platforms, with emphasis on formal verification capabilities, type system properties, vulnerability resistance, and ecosystem maturity. We analyze Solidity and Vyper (Ethereum Virtual Machine), Rust (Solana, Polkadot, NEAR), Move (Aptos, Sui), Cairo (StarkNet), Plutus and Haskell (Cardano), Michelson (Tezos), and Clarity (Stacks), evaluating each language against dimensions including static analysis properties, gas/weight models, resource management, concurrency semantics, and common vulnerability patterns. When viewed through the lens of High-Performance Computing (HPC), smart contract execution introduces unique challenges related to latency, transaction ordering, and maintaining global state consistency across a decentralized network. Therefore, the design choices within these languages—specifically concerning memory management, parallelism handling, and deterministic execution—mirror core concerns in distributed systems engineering. We analyze languages across major platforms, emphasizing their formal verification capabilities, type system properties, and runtime performance metrics relevant to distributed execution efficiency.