javascript and agda.
javascript has literally no type system, I know how to use it, and I can do functional programming or imperative programming comfortably in it depending on what's appropriate. javascript also doesn't half-ass having no type system like python does lol. because of typescript, js libraries have good documentation and autocomplete in vscode. js is actually my general purpose scripting language too because it has async/await so I can do stuff w APIs or files easily. it's a perfect language and I don't come across the pain points that a lot of people seem to on my own day to day of using the language.
agda has a dependent type system, and is a general purpose proof language. all proof languages suck ass including agda but agda makes sense to me and its interactive mode works for me the best. I also know how to use COQ now so I can't say I'd always reach for agda in every application but I definitely wish agda was the industry default instead of COQ





