amen zwa, esq.
I am an ordinary man, so I am unique up to isomorphism.
I am on MathsTodon not to preach to the choir, but to attend the concert.
I admire well constructed arguments, but I am not argumentative.
I always follow back valid accounts, but I do not chase down celebrities.
JD ⊥ MSCS ⏚ BSEE • GPS +38.89 -77.01 • CO₂ low 320s
Sarcasmaholics Anonymous | Burnistoun
Books on automated #ProofAssistants, like Coq, Lean, Agda, Idris, etc., fall into two groups: a vast majority aimed at working mathematicians and a handful aimed at programmers.
The following is a short list of #programming-focused #books (not short tutorials) on the use of proof assistants in crafting #verified software, categorised by type theory and listed in an approximate, ascending order of sophistication:
\(\textit{Coquand Calculus of Inductive Constructions}\)
• Introduction to Formal Reasoning (Lean), Altenkirch
• Programs and Proofs (Coq), Sergey
• Functional Programming in Lean, Christiansen
• Verified Functional Algorithms (Coq), Appel
• Certified Programming with Dependent Types (Coq), Chlipala
\(\textit{Martin-Löf Intuitionistic Type Theory}\)
• Certainty by Construction (Agda), Maguire
• Type-Driven Development with Idris, Brady
• Verified Functional Programming in Agda, Stump
• Programming Language Foundations in Agda, Wadler
• Software Foundations (Idris), Pierce
I recent saw a contractor "wrote" more than 500pp proposal in response to a federal agency's RFP. The document exhibits clear signs of having been generated by AI.
Guess how the agency contracting officers "read" that monstrosity: yup, AI.
It appears that in modern #IT, the only remaining entity who is still "thinking" and "learning" is the #AI.🤦♂️
Do even #MAGAt idiots listen to this imbecile anymore?
https://apnews.com/article/trump-pirro-reflecting-pool-3703eaedddf580f32ff9aca33bc11851
#F1 is boring. #RedBull is slumping. What should #Max do: stay at RB and pretend like all is well, switch to a team with better car, take a year sabbatical, or quit F1?
The most sensible, and arguably the most impactful, action that Max could take is to take a year off from F1 to wait it out for RB's improvement or for better teams' seats to free up. In the meantime, Max could hoist #GT racing to prominence, with at least three orders of magnitude more exciting than the present vapid, politics-ridden F1.