Jared Davis

About Me

I'm originally from Omaha, Nebraska. I studied computer science at UT Austin and completed my Ph.D. in 2009. I've worked at Centaur Technology (later acquired by Intel), Kookamara LLC, Apple, and Amazon, usually in formal hardware or software verification and security.

Stuff I've Built (pre-FAANG)

Milawa

My dissertation project, Milawa, was a self-verifying theorem prover. It starts as a small proof checker that can be extended with new proof techniques. The proof checker can verify these extensions so that they don't reduce our trust in the system. Through a bootstrapping process, the proof checker is extended many times and grows into an ACL2-like theorem prover.

Going beyond the prover itself, Magnus Myreen developed Jitawa, a verified Lisp runtime that is capable of hosting Milawa and running through its entire bootstrapping process. Magnus went on to prove, using HOL4, that Milawa is sound all the way down to x86 machine code when run on this Lisp! Our final, comprehensive Milawa/Jitawa paper is available in the Journal of Automated Reasoning:

The reflective Milawa theorem prover is sound (down to the machine code that runs it). Jared Davis and Magnus O. Myreen. Journal of Automated Reasoning. Springer. August, 2015. Volume 55(2), Pages 117-183.

Check it out!

Academic Papers

Some select publications:

• Fix your types. Sol Swords and Jared Davis. In ACL2 2015. October, 2015. EPTCS 192. Pages 3-16.
• Microcode Verification—Another Piece of the Microprocessor Verification Puzzle. Jared Davis, Anna Slobodova, and Sol Swords. Invited talk, ITP 2014. Springer, LNCS 8558. July, 2014. Pages 1-16.
• Embedding ACL2 Models in End-User Applications. In Do-Form 2013, AISB 2013, Exeter, UK. April, 2013. Pages 49-56.

Full list of publications, with abstracts.

ACL2 Projects

I've worked a lot with the ACL2 Theorem Prover, most of which is described in various sections of the ACL2+Books Manual. A few highlights:

• STD - Standard libraries for ACL2
• XDOC - Documentation system for ACL2 and its books
• VL - Verilog and SystemVerilog toolkit
• Bitops - Bit-vector reasoning library

Most ACL2 development happens at Github, see the Community Books project.

Aiksaurus

Circa 2000 I wrote Aiksaurus, an English-language thesaurus. I haven't worked on it in many years, but it appears to still be alive and well at Github. Most Linux users can also just:

• apt-get install gaiksaurus — GTK+ version (very good)
• apt-get install aiksaurus — command-line version

Stuff I've Enjoyed

Writing Advice

• Hemingway App — nice tool for initial, lightweight editing
• Joel Schwartzberg. Get to the Point! — tiny, useful book
• Be Succinct! (Writing for the Web)
• Betty S. Flowers. Madman, Architect, Carpenter, Judge: Roles and the Writing Process
• What Robert Mueller’s Peculiar Writing Style Tells Us About His Larger Legal Gambit
• Simon Peyton Jones. How to write a great research paper
• Simon Peyton Jones. How to give a great research talk

Book Suggestions

Some favorite books I discovered in 2024:

Top Picks

The Arbinger Institute. Leadership and Self Deception — deeply resonant

Cal Newport. Slow Productivity

Kim Scott. Just Work — a tour de force of lead with vulnerability

Yuval Noah Harari. Nexus — super interesting analysis of information and society

Tactical Advice

Richard Medcalf. Making Time for Strategy — crisp alternative to Slow Productivity

Rob Fitzpatrick. The Mom Test — short advice for better customer conversations

Michael Bungay Stanier. The Coaching Habit — superbly actionable advice for coaching better

Management

Kim Scott. Radical Candor — helpful mental model for being brave with feedback

Keith Ferrazzi. Never Lead Alone — thought provoking on how to amplify your leadership

Liz Wiseman. Multipliers — tedious but good, mostly mindset

William Pentak. The Way of the Shepherd — light, mostly mindset

Misc

John Bowe. I Have Something to Say — quirky, speaking lessons from toastmasters

Adam Grant. Hidden Potential — light but nice

Marcie Bianco. Breaking Free — can feminism aim beyond equality?

Some favorite non-fiction books about people, influence, and navigating organizations.

• Steven Covey. The 7 Habits of Highly Effective People — foundational
• Dale Carnegie. How to Win Friends and Influence People — dated, classic
• Robert Cialdini. Influence: The Psychology of Persuasion — awesome
• Daniel Kahneman. Thinking, Fast and Slow — interesting
• Adele Faber. How To Talk So Kids Will Listen and Listen So Kids Will Talk — widely applicable
• Chris Voss. Never Split the Difference
• Peter Drucker. The Effective Executive
• Tanya Reilly. The Staff Engineer's Path

Some favorite non-fiction books about management, strategy, leadership.

• Peter Drucker. Management — philosophical/historical
• Andrew Grove. High Output Management — thoughtful
• Richard Rumelt. Good Strategy / Bad Strategy — highly recommended
• John Lewis Gaddis. On Grand Strategy — awful in an awesome way
• Ken Blanchard. The New One Minute Manager — short, limited, very practical
• William Whyte. The Organization Man — quirky, fun
• Patrick Lencioni. The Five Dysfunctions of a Team
• Marcus Buckingham. First Break All the Rules
• Ryan Hawk. Welcome to Management — my first intro

Some less work-related favorite books are down in the grab bag.

Grab Bag

Just a pile of random stuff I've enjoyed. Not work related.

Obscure internet stuff

• The Gervais Principle, Or The Office According to ‘The Office’ — long, silly, fun
• The Codeless Code — koan-ish stuff for programmers, hit and miss
• Bret Victor. Magic Ink, The Future of Programming
• Mister Rogers Rules for Talking to Children
• EWD Archive — Dijkstra's proto-blog
• Dan Luu's Blog — often good
• Alastair Reid's Blog
• John Regehr's Blog
• Paul Graham's Essays
• Gary Bernhardt's Talks
• Guy Steele's “Growing a Language”
• Rich Hickey's “Simple Made Easy”
• The Cursed Computer Iceberg Meme

Some favorite podcasts around storytelling, history, etc.

• Scene on Radio — Seasons 2 (race), 3 (patriarchy), and 4 (democracy) are all strong recommends
• 1619 — Excellent
• S-Town — A beautiful, sad story
• Bundyville: The Remnant — Bundy family uprisings. Compellingly told
• Uncivil — Interesting civil war stories
• More Perfect — Stories about interesting Supreme Court cases
• Hardcore History — Very nice storytelling (Rome, WWI, Supernova in the East)

Some favorite podcasts around current events.

• Southlake — Race and school debates, etc.
• Ezra Klein Show — Thoughtful political podcast
• Vox Conversations
• Citations Needed — Leftist politics
• The Dig — Leftist politics, hit and miss
• Fresh Air — Interviews, hit and miss depending on the guest
• Reveal

Some favorite podcasts around management/leadership.

• Coaching for Leaders — consistently good, great source of book leads
• The Learning Leader — often good

Misc favorite podcasts.

• Exponent — Business, strategy, disruption. Hit and miss
• CoRecursive: Coding Stories — Interviews with programmers

Some favorite non-fiction books about society, history.

• Heather McGhee. The Sum of Us — masterful
• Nell Irvin Painter. The History of White People — dry, damning excellence
• Isabel Wilkerson. Caste: The Origins of Our Discontents
• Barbara W. Tuchman. The Guns of August — great history of WWI
• Garrett G. Fagan. The History of Ancient Rome — nicely done lecture series (audiobook)
• Jared Diamond. Guns, Germs, and Steel — dry but expansive history of humanity

Some favorite fiction books, mostly sci-fi and fantasy.

• Adrian Tchaikovsky. Children of Time
• Robert Charles Wilson. Spin; Blind Lake
• Vernor Vinge. A Deepness in the Sky — and many more
• Ursula K. Le Guin. The Dispossessed; The Lathe of Heaven; everything else
• Sherri Tepper. Grass; The True Game; The Awakeners
• Ernest Hemingway. For Whom the Bell Tolls — beautiful, not sci-fi
• Roger Zelazny. Lord of Light; Amber
• Isaac Asimov. Nightfall; Nemesis; Foundation