The field of formal methods and programming languages is experiencing significant advancements, driven by the increasing importance of formal verification and the need for more expressive and flexible programming languages. Researchers are exploring new approaches to integrate natural language and formal methods, enabling the development of more intuitive and accessible programming languages. Another area of focus is the application of large language models to automate semantic analysis and provide instructional guidance. Additionally, there is a growing interest in developing tools and platforms that support collaborative feature modeling, step-by-step verification, and rule-based derivation construction. Notable papers in this area include LeanTutor, which presents a formally-verified AI tutor for mathematical proofs, and Linguine, a natural-language programming language with formal semantics and a clean compiler pipeline. Furthermore, papers like StepProof and Hazel Deriver demonstrate innovative approaches to step-by-step verification and derivation construction, respectively.