Untitled attachment

Notices where this attachment appears

1. Embed this notice
   Paul Cantrell (inthehands@hachyderm.io)'s status on Friday, 01-Dec-2023 01:47:58 JST Paul Cantrell

   in reply to

   @penguin42 @edavies @thephd
   …you end up passing around •mathematical proofs• as part of your programming language, which are machine-generated and/or human-written + machine-verified.

   It’s a grandiose, confusing dream that is either The Future of Programming™ or a quixotic research exercise, depending on who you ask.

   If you’re wondering what it looks like in practice, Lean might be a place to start:
   https://lean-lang.org