(as an interested university student:) From Programming at a small scale in Javascript and Logo¹, I have gathered that not knowing what type something is can be annoying. They also have REPLs, which is pretty nice. From various blog posts and debugging Rust programs, I have learned that not having a REPL can be annoying. Are there languages that have both?
(¹ Logo is a “lisp” with omitable parentheses, where these also don’t define runtime-mutable s-expressions, lists are in brackets, and also Logo doesn’t have structs, giving it bad maintainability outside of not having Type Annotation too)
Candidates
- C# : Does it have a repl?
- Java in BlueJ somehow
- sometimes people just put Lisp or Lua in their C/Rust++ program (emacs, shenzhen I/O(game)), this accomplishes a similar task of making some debugging or scripting code faster to compile/interpret, but slower to run


Modules are called such because they enable modularity. https://www.pathsensitive.com/2023/03/modules-matter-most-for-masses.html?m=1 that link will explain it more thoroughly than I want to or probably could.
Ah ok, we’re getting into Coq proofs. I’m trying to work through Software Foundations but it’s so tricky! I feel like I need an intellect potion to get it