https://www.europesays.com/uk/10331/ High-performance computing, with much less code | MIT News #Computing #Cursors #Exo2 #HighPerformanceComputingLanguage #JonathanRaganKelley #MetaProgramming #MITCSAIL #PerformanceEngineering #Technology #TheoremProvers #UK #UnitedKingdom #UserSchedulableLanguages #YukaIkarashi
I'm trying to use Z3 to solve a logic puzzle, mostly as a chance to learn more about Z3. I'm stuck on a couple of things out of the gate:
How do people usually interact with Z3 in practice? Manually writing smtlib doesn't seem like it would scale. Do people use the Z3 bindings to Python, Java, etc. or are people using libraries to generate smtlib syntax which then gets fed in?
I'm looking at the TypeScript bindings. There's a "high level" set of bindings which seems incomplete (no support for datatype declarations, for example) and a "low level" set of bindings that seems more featureful. I get the vibe that the high level bindings aren't getting a lot of usage or maintenance. Can anyone confirm or give background here? Is TS simply the wrong language to use, or am I still likely to be writing Z3 in a modern-ish way by using the low level bindings?
Extended abstract by Sára Juhošová at TyDe '24: How Novices Perceive Interactive Theorem Provers
"we conducted an online survey among bachelor students, asking them to list the obstacles they encountered while learning Agda. [...]These observations point to one prominent point of improvement: providing a more accessible and sturdy infrastructure for ITP programmers."
My PhD student Sára and I are looking for people to participate in a study on usability aspects of interactive theorem provers. Please consider signing up!
Who? anyone who uses or has used an interactive theorem prover for whatever purpose
What? 90 - 120 minute interviews (possibly including a small think-aloud programming session)
When? interviews will be scheduled starting September 2024
Where? online (participants from anywhere are welcome)
We are hoping these interviews will help us determine how you interact with your theorem provers and to gain insights on how we can improve the user experience. We are interested in all aspects of interactive theorem provers, including but not limited to their design, their tooling, their libraries, and their documentation.
Sign up here: https://tudelft.fra1.qualtrics.com/jfe/form/SV_0UJKuqcWC9G4FEy
"Concerning computer assisted proofs, it seems to me the main obstacle is user friendliness; if you want this to become a part of the culture of mathematics, that when you submit a paper it includes a computer verification that the paper is correct -- I think this is very unlikely to become a part of the culture of mathematics, but if you want it to -- then, what you need is proof assistants that mathematicians are willing to use, so that it doesn't take 100 times as long to provide that certificate as it does to produce a paper the usual way."
- Jacob Lurie
There are some (seemingly obvious) real-world applications of interactive #TheoremProvers like #lean that honestly have the power to change the world, we just have a broken social system that wont properly invest in them. For example, I imagine that carefully crafted curricular mathematics teaching languages ala #HTDP for K-12 (with perhaps a scratch-like interface for the younger kids) created in lean would be a game-changer for mathematics education.
I was lucky enough to be sent to a decent public school for #autistic and #ADHD kids growing up, because I had consistently done terribly at math in school because I couldn't sit still, keep my mouth closed, and was constantly in ISAP, but I always scored in the top percentage of standardized tests. There I got to do mathematics self-study, with a teacher to help when needed, and that was truly liberating, and I graduated early with an almost 4.0 grade point average, and went on to do an (unfinished) philosophy doctorate, much of which involved category theory. I feel like if kids had an environment to independently explore #mathematics, one that grows with them, many kids that are bad at it now would succeed.
