Michael Shulman also wrote about the extension to Homotopical Trinitarianism [2]

For a good summary with links there is [3]

[1] Computational Trinitarinism, https://existentialtype.wordpress.com/2011/03/27/the-holy-tr...

[2] Homotopical Trinitarinism, http://home.sandiego.edu/~shulman/papers/trinity.pdf]

[3] nCatLab, https://ncatlab.org/nlab/show/computational+trilogy

For verification with proof assistants, [Software Foundations](https://softwarefoundations.cis.upenn.edu/) and [Concrete Semantics](http://concrete-semantics.org/) are both solid.

For verification via model checking, you can check out [Learn TLA+](https://learntla.com/), and the more theoretical [Specifying Systems](https://lamport.azurewebsites.net/tla/book-02-08-08.pdf).

For more theory, check out [Formal Reasoning About Programs](http://adam.chlipala.net/frap/).

And for general projects look at [F*](https://www.fstar-lang.org/) and [Dafny](https://dafny.org/).

Alternatively you may enjoy these two. The latter is especially thorough, and begins with classical logic:

* Concrete Semantics (Isabelle): http://concrete-semantics.org

* Program = Proof (Agda): https://www.lix.polytechnique.fr/Labo/Samuel.Mimram/teaching...

[0] https://www.cis.upenn.edu/~bcpierce/tapl/

If you have a particularly generous definition of hero, then you might not be asking too much

[0] read: natural language

I was so disgusted by the tutorials for Coq that I wrote my own. It has been reviewed positively on Hacker News before. If you want a look at some of the basics of formal proof and these tools, take a look:

http://michaeldnahas.com/doc/nahas_tutorial.html

my bad, I was using a "slangy" sort of description to say "shouldn't somebody read the textbook that would be used in a computer science 101 class (or a math 101 class) except not 101 but a hypothetical 3rd level class" so I called it 301. I was asking, "what textbook is used in an upper level undergraduate course on the topic?"

Many American universities use a numbering system of 101 & 102 for the fall and spring term classes somebody majoring in the subject would take, and 201 - 202 for the 2nd year. A CS100-level class would be a lighter survey for somebody who would want to study some CS but not major in it.

The typing statement has to be proven by realizing the isomorphism demanded by substitution. You are more than anything directly proving what you claim in the type. Since proof is isomorphism here, the computation in terms of lowering the body of the definition to a concrete set of instructions is execution of your proof! (possibly machine code or just abstract in a virtual machine like STG). The constructive world is really nice. I hope the future builds here and dependent types with univalence is made easier and more efficient.

[1]https://www.idris-lang.org [2]https://homotopytypetheory.org/2012/01/22/univalence-versus-... [3]https://redprl.org

Assume that regular software has, on average, one bug every 50 lines. (All numbers made up on the spot, or your money back.) Let's suppose that Idris can reduce that to absolutely zero. And let's suppose that totally-working software is worth twice as much as the buggy-but-still-mostly-working slop we get today.

But Idris is harder to write. Not just a bit harder. I'd guess that it's maybe 10 times as hard to write as Javascript. So we'd get better software, but only 1/10 as much of it. Take your ten most favorite web applications or phone apps. You only would have one of them - but that one would never crash. Most people won't make that trade. Most companies that produce software won't make it, either, because they know their customers won't.

Well, you say, what about safety-critical software? What about, say, airplane flight control software? Surely in that environment, producing correct software matters more than producing it quickly, right?

Yes, but also you're in the world of real-time embedded systems. Speed matters, but also provably correct timing. Can you prove that your software meets the timing requirements in all cases, if you wrote it in Idris? I believe that is, at best, an unsolved problem. So what they do is they write in carefully chosen subsets of C++ or Rust, and with a careful eye on the timing (and with the help of tools).

So given that context, it doesn't sound to tough to add a cost to the type for each operation, function call, whatever, and have the type checker count up the cost of each call. So you'd have real proof that you're under some threshold. I wouldn't put the agda runtime on a flight control computer. But I think I could write a compiler, now, For like a microcontroller that would count up (or spend time budget, doesn't matter).

A more sophisticated computer would be way way harder, and be resource efficient. But if you modeled it as "everything's a cache miss" and don't mind a bunch of no-ops all the time, that would be a pretty straightforward adaptation of the microcontroller approach.

There are features in Agda/Idris (and probably Coq, about which I sadly know almost nothing) that are absent from Lean and are useful when programming (coinduction, set omega, more powerful `mutual`, explicit multiplicity, cubical? etc), but I'd say the need for them is less common.

How much software do you think we need? 10x less sounds about right to me.

Verification proves that software works according to its "spec". But is the spec "correct"?

Writing NON-formally-verified software 10 x faster means you have a much better chance of figuring out how you should fix your spec.

1: https://arxiv.org/abs/2210.08232

2: https://chat.openai.com/share/aadb7a0a-08a4-4951-b877-cb2f61...

[0] https://research.microsoft.com/en-us/um/people/lamport/pubs/...

λf :(τ 1 × τ 2 ) → τ 3 .λx:τ 1 .λy:τ 2 .f (x,y) has type ((τ 1 × τ 2 ) → τ 3 ) → (τ 1 → τ 2 → τ 3 ).

Yeah, that's accessible.

Let's do this in Python. First, write a function that curries:

  def curry(f):
      def g(x):
          def h(y):
              return f(x, y)
          return h
      return g


  my_func = lambda x, y: 10 * x + y
  curried = curry(my_func)
  print(curried(5)(3))
  # output: 53

  from typing import TypeVar, Callable

  A = TypeVar('A')
  B = TypeVar('B')
  C = TypeVar('C')

  def curry(f: Callable[[A, B], C]) -> Callable[[A], Callable[[B], C]]:
      def g(x: A) -> Callable[[B], C]:
          def h(y: B) -> C:
              return f(x, y)
          return h
      return g

  Callable[[Callable[[A, B], C]], Callable[[A], Callable[[B], C]]]

In other words, baloney. If you don't do that kind of programming, that stuff is very opaque. I might be able to get it if I were willing to stare at it for another 15 minutes, but I'm not willing.

That part.

– Lambda calculus tutorial that gets you up to what you need to understand the referenced paper in 15 minutes

- A description of Hoare notation that I can also understand to adequate depth to understand the referenced paper, also in 15 minutes

- A description of classical logic etc. etc. 15 minutes

- A description of intuitionistic logic etc. etc. 15 minutes (presumably in how it differs from classical)

These would be very useful. If you can also explain them in a way that would allow me to use the information I've learnt in an hour to do something useful with programs like represent them, transform them, verify them against a specification, I would gladly spend a couple of weeks or a month doing that, genuinely.

If you can't do any of these things, please stop posting how easy it all is

which, this?

"We saw earlier in the course that we can curry a function. That is, given a function of type (τ 1 ×τ 2 ) → τ 3 , we can give a function of type τ 1 → τ 2 → τ 3"

That helps no-one unless you have some serious hand-holding. I know the type of curry, I've written curry/bind/whateveer in C#, scala, JS and likely others. I have a background in this. It's not 'accessible' to mere mortals and even I'm not familiar with some of the notation here. Stop pretending it's just laziness on other people's part.

(oh yeah, did I forget to put constructive logic in my list above? Brouwer's intuitionism? FFS get real, I never even heard of that until a few years ago)

There's something of Cassandra about it.

You can curry a function (supply its arguments one-by-one instead of all at once).

You have:

  f(x, y) which has type (τ1 x τ2) -> τ3

  f x y which has type τ1 -> τ2 -> τ3

  λx. λy. f(x, y)

  ((τ1 × τ2) → τ3) → (τ1 → τ2 → τ3)

  (A ∧ B ⇒ C) ⇒ (A ⇒ (B ⇒ C))

> Since this logical formula is a tautology

You forgot to say 'obviously' /s

[1] https://maa.org/press/maa-reviews/principles-of-mathematical...

This one doesn't need that.

"Accessible" doesn't necessarily mean "with just knowledge of English, you can jump to this example and immediately understand what it means". Some work is always required; accessible just means this work is not too hard.

For example, Python's notation has been occasionally described as "accessible", yet I wouldn't expect my mum to immediately understand a non-trivial Python snippet (so no "print('hello')") without any previous explanations.

It can probably be called accessible for people already interested or talented in maths, but there's a reason most people don't just casually learn astrophysics for fun even though some introductory material might be considered accessible - not everyone can do it without unreasonable amounts of effort.

Oh, I'm not saying it's the same as programming in your favorite language.

I'm saying if you have the mental machinery to understand a new language, you also have it to learn lambda calculus. Trust me, it's not that hard. It just looks extraneous out of context because you are not familiar with it.

> It can probably be called accessible for people already interested or talented in maths

I'm not particularly good at maths and I found introductory-level lambda calculus not very difficult. The notation is different from, say, a C program. You just learn this notation, which your professor will explain. Nothing too terrible.

> layers of abstraction

I'm confused. Which layers of abstraction? I mean, it's an abstraction just like C or Python or "1 + 1" are abstractions. There are rules and you learn how to apply them.

Now, the next bit – so I've spent my 15 minutes reading up on each of these formalisms (lambda calculus, intuitionistic logic, Hoare notation, whatever else). So now I can read the paper and I do, and now I have absolutely no way of making use of anything I've learnt. I spent personally a lot of time on the computer science side of things, and I have got frankly just about nothing out of it. So frankly again, there's no point learning it (from a utilitarian perspective).

When I was a kid I picked up a book on Fortran 4 and tried to learn it from the book, without a computer. That's pretty much the situation here – a passive notation that, had I managed to internalise it, would have been completely useless because I had no computer to run it on. And I'm tired of this discussion of people saying it's easy and it's useful, because it's not easy, and it's not useful without a whole lot more studying an application to bridge the abstraction of the formalism to the actual programming environment where I can use it.

Please just stop repeating stuff.

You started out saying, "oh, these lecture requires some advanced math background to understand", and quoted the curry function. And then a lot of people explained that no, there is no advanced math, this is just a function written in a programming language. And now it seems you agree, if you spend only 15 minutes you can understand the lecture notes. That's all I, and others, wanted to say.

Separately, it's the case that understanding this will not be very useful in a day-to-day programming job. That's just because it's not all that useful! (See other discussion on this this same HN page.) I think it is very cool and philosophically interesting in itself, and it offers an interesting point of view if you are designing new programming language type systems, but it doesn't have very much "utilitarian" use.

that was sarcasm.

> I think it is very cool and philosophically interesting in itself, and it offers an interesting point of view if you are designing new programming language type systems, but it doesn't have very much "utilitarian" use.

It has phenomenal use is my point (eg. formal verification, an interest of mine), but only at a vastly higher level than "I've been to the lectures". What I keep saying is, most people aren't interested in the abstract, and neither am I. Give me a practical application and suddenly I'll 'get it'. Without that application it's valueless because I have no reason to engage with it, and actually cannot. Put another way: its application and its understanding are interlinked. You can separate them; I and others can't.

I know this stuff is useful and I literally spent years trying to understand it. For someone like me it just isn't easy, and you keep persistently not understanding that.

Given that there's this correspondence between Math and Programming Languages, what it says is just that if you understand types in programming language, there's no point in understanding the notations in math.

And this is especially true if you take a cynical attitude towards theorem provers in the sense that real proofs are in the minds of the thinker, not in the formalism.

The fact that the Curry-Howard correspondence is was proposed in the 1930s suggests that it was a relatively "primitive" analogy that might be restated in some obvious way in today's language of computation. Maybe... "you can write programs to be automated theorem provers for formal systems"?

I wonder what CS people would have to say about the efforts "to prove a program correct". If a program is equivalent to a proof, "proving a program correct" seems to be "proving a proof correct".

I don't really know what I'm talking about though.

I think there are several different types of ‘background’ required to read something, none of which are innate or unattainable without a particular kind of education (e.g. a university degree). This confuses discussions about whether something is ‘accessible’ because the person complaining that it is inaccessible might be complaining of a gap between their current state and the state assumed by the book, in any of those three categories.

1) Factual background.

What facts do you need to know, what theories do you need to understand, in order to be able to follow what the author is saying? If the author is trying to teach you classical mechanics but you don't know about addition, you're not going to get very far until you go and learn to add and come back.

A source can address this (reducing the amount of background required) by providing more background in the material itself. But it obviously doesn't scale that well if every explanation of classical mechanics comes with an explanation of addition (and counting, etc.), and the background you do get, if it isn't the primary goal of the material, is often rushed and not as well-written as a dedicated source. So instead (or as well as providing a quick refresher for people who already have the background but might have forgotten it) authors will often refer to other materials that provide better explanations.

Inaccessibility arguments from this perspective look like ‘I don't know what this word means’ or ‘I don't know how to read this notation’.

2) Motivational background.

What applications do you need to know about in order to find out worthwhile to learn a topic? If you don't know about bicycles, levers, etc., learning about classical mechanics can seem like an abstract waste of time.

As a function of the complexity of a topic, it necessarily takes a certain amount of time before the author's thoughts are complete enough to relate to something that the reader will find compelling, though a good author will try to minimize it. People vary here in their trust of an author, and there are certain external factors that can influence this as well: e.g. if the material is very well-regarded by other people the reader might be happier to spend time figuring out what it's trying to say, or if the reader has a background in a similar topic they might be able to imagine some motivations that will keep them going.

That's not to say that the reader should always have this: indeed, most materials are actually useless to most people. One of the pre-tasks of reading something is deciding whether it's something that is (potentially) even useful to read, and for most things your answer should be ‘no’.

Inaccessibility arguments from this perspective look like ‘I don't care about this’ or ‘this is abstract nonsense’. Note that text is never actually completely abstract: authors, like readers, are always motivated by practical concerns. But there might be a long chain of problems and solutions from a problem that the reader is aware of to the solution that the author is explaining — in fact, in pure maths, the applications of a theory aren't always even known — but there's good reason to believe that they exist.

3) Attention span.

Difficult concepts just take a long time to learn. This can be addressed somewhat in the text by providing longer explanations in which the concept is spelt out more elaborately, but then you risk alienating readers who've lost track of your point by the time you've got to the end of it — there's a balance to be struck, and the correct point on the continuum depends on your intended readership. Also, on the reader's end, this is to some extent a ‘muscle’ that needs to be trained and regularly exercised in order to not lose it.

All of these things lead to valid arguments of inaccessibility, but the failure isn't inherent in the writing: instead it indicates a mismatch between the writing and the reader. If the writing means to target a certain type of reader, that can make it badly written; but no writing can target every possible reader. If some writing seems inaccessible for you, if you're interested in it you can work on those three things to make it more accessible (which will involve some combination of staring at the target writing until it makes sense, and reading around related writings to get knowledge and practice reading about that kind of thing). Alternatively, you might be able to find other writings on the same topic with prerequisites that are a better match to you. For example, I've been trying to write a series of posts explaining CS concepts that I think are cool or useful, assuming the knowledge and motivation of an enterprise programmer, and drawing the chain of motivation/explanation as far back as necessary to get to concepts they're likely to know already. My writing on the lambda calculus is here:

https://twey.io/for-programmers/lambda-calculus/

Please excuse the sloppy writing, this is an attempt to get back into technical/explanatory writing after many years — but criticisms (with that particular intended audience in mind) are very welcome!

One way to think about it, is that proofs about a program are a continuum, rather than one or the other. Sure, going all the way, disallowing mutability and requiring types for everything, might make the system more provable, but slower as well.

There are some different ways to look at a program:

Corporate developer: "Programs are to be run, and occasionally read or proved correctly" Donald Knuth: "Programs are to be read, and occasionally run" Type Theorist: "Programs are to be compiled, and occasionally run or read"

https://thenewstack.io/rust-in-the-linux-kernel/

https://security.googleblog.com/2023/10/bare-metal-rust-in-a...

You're clearly highly intelligent, evidently more so than I am. Additionally my mind doesn't work like yours, I'm not an abstract thinker. Plonk stuff like this in front of me and I can decipher it eventually, if I can get some clear statement of the notation and its semantics anyway, and there is stuff in there I'm not familiar with.

Most people aren't abstract thinkers. They are motivated by practical concerns. I spent an enormous amount of time reading up on stuff like this and I really can't see the value to it to me as a programmer. It's deeply frustrating because I know it has value, but I just can't use it. It's interesting, I know it's useful, but I can't use it.

Please allow that other people think differently and are motivated differently, and don't assume that what's easy for you is for them. I wish I had your cranium.

Humble, respectful, modest?

I respect that different people will find different things hard or easy, so that a generalization is never truly possible (except, uh, this sentence?). On the other hand, speaking with absolutely no generalizations whatsoever is simply not possible, because so many caveats and exceptions would make communication impossible.

I do stand by my initial assertion that, in general, if you have a mind capable of learning a new programming language, you can learn lambda calculus, and it won't be particularly hard.

Abstract thinking is motivated by practical concerns, namely being able to think comfortably about larger problems without being limited by one's capability for complex reasoning. Most people don't do it because they aren't used to, or they have never been taught how.

Don't talk rubbish about 'look it up'. You need a degree to get this. Not a metaphorical degree, the real thing.

Edit - and a brain bigger than mine.

You really don't need a degree. The Curry-Howard isomorphism is taught in undergraduate CS courses, to students who are simultaneously being introduced to lambda calculus.

While I wouldn't say it's trivial, it's not rocket science either. Most students get it and pass the exams.

Now I just wish there were something similar for the missing category theory third of the trinitary mentioned in another comment.

Business really interferes with the goal of the mathematical programmer — proofs of concept, hacks to get MVPs over the line, throwaway demos to investors etc. — but after a certain point the value of the codebase becomes entrenched into the value of the business and that’s when you need to bring in the mathematical coders to constantly refine and prune your codebase into something that will survive and bear out the earnings per share values.

I don't get it. Or rather, I don't get the significance of the Curry-Howard Isomorphism. Questions:

1) Is there an example of a proof and its corresponding program that makes you say "whoa, trippy, I didn't expect those to be related"? Like, yeah, an Int -> Boolean function "proves" you can construct a Boolean from an integer, but ... so what? What would a non-trivial proof (say, on the order of the Pons Asinorum) look like as a program?

2) Are the "programs" referred to here to merely pure functions (i.e. side effect-free, global state-free ones)? It sounds like it is based on lines like this:

>When a computer program runs, each line is “evaluated” to yield a single output.

That ... seems to cram "computer programs" into some kind of Procrustean bed unless we're taking about pure functions. But then it also talks about how CHI has applications in verifiable programs, which, I'm told, can reason about side effects.

Feel free to call me an idiot, as long as you can also inspire an aha-moment.

* Every type system is a system of logic (and vice-versa.) * So, if you have a System F, you can build a Haskell. * If you have affine logic, you can make Rust.

Have a look at this parser combinator library[1]. In particular look at how many functions are marked "Totality: total". These are functions which accept all (well-typed) inputs and terminate in finite time.

> What would a non-trivial proof (say, on the order of the Pons Asinorum) look like as a program?

It would just be a program - that you write every day. If Pons Asinorum is expressed in twenty lines, then pick a twenty-line program. If you want something bigger, check out CakeML or seL4.

> But then it also talks about how CHI has applications in verifiable programs, which, I'm told, can reason about side effects.

Not every effect is a side-effect. A suitable definition of "side-effect" might be "an effect which is able to punch a hole through whatever type system decided it was valid." If your programming language represents effects as types, then it can reason-about/type-check them just as well as pure functions.

[1] https://www.idris-lang.org/docs/idris2/current/contrib_docs/...

That seems to be different from CHI, which asserts a correspondence between proofs and programs, not between systems of logic and languages; if the latter is more general it probably should have, and would have, been phrased that way.

>Have a look at this parser combinator library[1]. In particular look at how many functions are marked "Totality: total". These are functions which accept all (well-typed) inputs and terminate in finite time.

Sorry, what's the connection to CHI here?

>It would just be a program - that you write every day. If Pons Asinorum is expressed in twenty lines, then pick a twenty-line program. If you want something bigger, check out CakeML or seL4.

I meant "non-trivial" to apply to the mapping as well. As best I can tell, CHI just says there's some useless program that maps to every proof, and a useless proof that maps to every program. So what? What is the significance of that? So I can write a meaningless program that corresponds to Pons Asinorum?

You're not really taking the challenge seriously here -- you're just asserting the same trivialities about which I was asking, "is that all there is?"

But proofs are written in systems of logic and programs are written in (programming) languages, so if there's a correspondence between the first there really ought to be a correspondence between the second!

And if your return type is something other than Boolean, that represents some more general construction rather than mere decidability. But everything else is just about the same. Of course this all assumes a total language with no general recursion, since otherwise you can "prove" anything by just looping forever and not delivering a result.

It would have to be all, not just some, or it's not an isomorphism (or there are caveats about function purity I mentioned before).

>"Apply Lemma f to variable x with preconditions given by H1, H2; call the resulting statement L" is equivalent to a function call L = f(x, H1, H2) where H1, H2 are capabilities or abstract "tokens".

Okay, that helps. So where are the mind-blowing examples?

Hopefully my made up syntax is understandable

  fermat x y z: Int -> Int -> Int -> c: (x^z+y^z=c^z and Int)

"Infinite search in finite time" https://math.andrej.com/2007/09/28/seemingly-impossible-func... https://math.andrej.com/2008/11/21/a-haskell-monad-for-infin...

There are some connections in mathematics that are quite "magical", where you get something like a correspondence between a family of curved surfaces and a family of integer-valued equations, and it's not at all obvious why that might be until you study it deeply.

And sometimes articles about the Curry-Howard Isomorphism suggest that it's an example of that sort (I think this article does, to some extent).

But (as I understand it), that isn't the case: here we have a simple directly-constructed correspondence. It's valuable, but not the sort of thing that mathematicians think of as a wonderful result.

1) The trippy one I know of is that the Church encoding of numbers is the induction principle for naturals.

2) Generally the programs that are proofs you would want to be pure, but it wouldn't be strictly necessary. The impurity would have to be handled by the type system though, so explicit effects not side-effects.

Also, note that even though you want the programs-that-are-proofs to be pure, that doesn't mean you can't prove things about programs that are impure - that is, you have a pure-program that has a type, and that type is a proposition about a different impure program.

That is, I can create a pure program that is a proof about my impure program.

EDIT: I think something that is a sticking point for a lot of people is looking for a program that is useful by itself that is also the proof of something useful. This is possible, but a bit rare-er - oftentimes you have useful programs with trivial types, or useful programs-that-are-proofs that you don't actually care to run. These are still super useful though! It is possible to have ones that are both - decidability of things is what comes to mind. You could write a program that determines if two naturals are equal - that's a useful program, albeit one of the simplest - and that program also serves as a proof that two naturals are either equal or not - a kind of particular instantiation of the law of excluded middle. One style of programming with dependent types always returns a proof along with the returned value, which might be kind-of what you're looking for. (Think of a regular expression engine that along with the yes/no does this string match this regular expression, returns a proof that the string does or doesn't match, demonstrating its own correctness)

When you compute a pure function, you’re still physically manipulating registers, cache, etc.

You can use the proof-program perspective to formalize reasoning about a program:

- you have some domain model; this expresses the “business logic” of your software

- you have an abstract model, in a category for your programming language; this expresses an equivalent structure as the “business logic”

- you have a concrete model, in a category for your hardware; this expresses an equivalent structure as it gets executed

Reasoning about the translations between these steps, their properties, etc is why you want to connect software to proofs.

For example, if you want to find an optimal implementation: you want the shortest path of atomic arrows in your hardware category, which corresponds to the desired computation in your language category.

Category theory is the language in which we connect our theory of hardware to our theory of the business domain!

Theorem: For any function g from a convex, compact set to itself, there exists a fixed point of g.

program f: g --> x where g is a function from a convex, compact set C to itself, and x satisfies g(x) = x.

If you can write the program and it is correct for all such g, that is a proof that such a g always has a fixed point (in particular, you output one). Note the "type" of g is "function from convex, compact set to itself" and the "type" of x is "fixed point of g".

    loginAdmin(name: &str, password: &str) -> Result<Admin, AuthenticationError>
    deleteDatabase(admin: Admin, dbConnection: &DbConnection, dbName: &str) -> Result<(), ConnectionError>

    let evilAdmin: Admin = unsafe { std::mem::transmute([0; size_of<Admin>()]) };
    deleteDatabase(evilAdmin, dbConnection, "important_data");

    anything : a
    anything = recurse 0
        where recurse i = recurse (i + 1)

    data Nat where
        0 : Nat
        S : Nat -> Nat  -- n + 1, "S"uccessor

    data Vec (n : Nat) a where
        Nil  : forall a, Vec 0 a
        Cons : forall n a, a -> Vec n a -> Vec (S n) a

    -- Instances of `IsTrue b` only exist if `b = True`
    data IsTrue (b : Boolean) where
        Trivial : IsTrue True

    -- Instances of `Every pred vec` only exist if every element in `vec` satisfies the predicate (so that `pred elem = True`)
    data Every (pred : a -> Boolean) (vec: Vec n a) where
        Every_nil : forall pred, Every pred Nil  -- Every item of an empty vector satisfies an arbitrary predicate
        -- Prepending an element which satisfies some predicate to a vector where every element satisfies the same predicate, produces a vector where every element satisfies the same predicate
        Every_cons : forall pred x xs, IsTrue (pred x) -> Every pred xs Every pred (Cons x xs)

    foosAreFoo : Every (\n -> n == "foo") (Cons "foo" (Cons "foo" (Cons "foo" Nil)))
    foosAreFoo = Every_cons Trivial (Every_cons Trivial (Every_cons Trivial Every_nil))

    head : Vec n a -> a
    head Nil = ???
    head (Cons x _) = x

    head : Vec (S n) a -> a
    head (Cons x _) = x
    

    data Var a = String

    -- Example IO monad which represents side-effects (stdin, stdout, and variables) through constructors
    data IO a where
        Pure      : a -> IO a
        ReadLine  : IO String
        PrintLine : String -> IO ()
        ReadVar   : Var a -> IO (Maybe a)
        WriteVar  : Var a -> Maybe a -> IO a
        (>>=)     : IO a -> (a -> b) -> IO b

    -- "Pure" program which reads first and last name and prints full name.
    -- The "interpreter" lazily computes the value of `main` and simultaneously evaluates `IO` actions to get their inner values:
    -- When it encounters (x >>= y) it computes `x`, evaluates `x` to get the inner value at runtime,
    -- then computes and evaluates `y`
    main : IO ()
    main =
        PrintLine "What is your first name?"  >>= \() ->
        ReadLine                              >>= \firstName ->
        PrintLine "What is your last name?"   >>= \() ->
        ReadLine                              >>= \lastName ->
        Pure (firstName ++ " " ++ lastName)   >>= \fullName ->
        PrintLine ("Hello " ++ fullName ++ "!")

    foo : Var Int
    foo = Var "Foo"

    -- Proving properties of programs is done with Hoare Logic.
    -- This is a lot more complicated and full of boilerplate...
    data Predicate where
        True  : Predicate
        (!==) : forall a, Var a -> a -> Predicate
        (/\)  : Predicate -> Predicate -> Predicate
    data HoareTriple (pre : Predicate) (stmt : IO ()) (post : Predicate) where
        Obvious  : forall pre stmt, HoareTriple pre stmt True
        Merge    : forall pre stmt post1 post2, HoareTriple pre stmt post1 -> HoareTriple pre stmt post2 -> HoareTriple pre stmt (post1 /\ post2)
        WeakenL  : forall pre1 pre2 stmt post, HoareTriple pre1 stmt post -> HoareTriple (pre1 /\ pre2) stmt post
        WeakenR  : forall pre1 pre2 stmt post, HoareTriple pre2 stmt post -> HoareTriple (pre1 /\ pre2) stmt post
        Specific : forall varN n, HoareTriple (varN !== n) (ReadVar varN >>= \nValue - WriteVar (varN + 1)) (varN !== (n + 1))
    example : HoareTriple
        (foo !== 4 /\ foo !== 5)                                -- Precondition
        (ReadVar foo >>= \fooValue -> WriteVar (fooValue + 1))  -- Statement
        (foo !== 5 /\ foo !== 6)                                -- Postcondition
    example = ...  -- Some combination of Merge, WeakenL, WeakenR, and Specific, but I've written enough

ps. and our calculators (& excel) needs better support for it

Did your highschool physics not have this? I always thought it was a universal part of all physics education. Doing things like canceling out units etc. has always been a big part of high school physics, and checking that your final answer has the units it should. (If it didn't, you made a mistake somewhere.)

The idea of building units into Excel is definitely an intriguing one, though. I'm honestly kind of surprised it's the first time I've ever heard it suggested. It does seem like a pretty useful idea.

Gotta love that USA's 'A'P classes' entire curriculum are Chapter 1, p.1 everywhere else.

I can't imagine any HS science class not already doing this. It would be impossible to answer many, if not all, of the questions correctly if you mix units (either unit-kind like mixing time and distance units, or unit-scale like mixing seconds and hours).

Your point about tools that support units is great. Reminds me of https://frinklang.org/

For example, what is the type of the / operation such that 4m/2s = 2m/s, but also 4kg/2kg = 2?

It's not impossible of course, but it is highly tedious and complex to actually define these types in a formal way.

Not to mention, linear algebra (matrix operations) gets REALLY ugly to define formal types for really fast if you allow different measurement units for every matrix element, like you often do in physics.

And, just like the others, I never met a physics class that didn't enforce unit maths at every step of computation, starting in sixth grade.

But this is done with a simple informal system, not type theory of all things. The informal system of measurement units being essentially to treat the units as special values that act as factors and obey all the usual rules of multiplication and division, and don't allow addition or subtraction.

Types as such are dealt with as sets. So for example I'm working my way through Serge Lang's "Basic Mathematics" at the moment[1], and it starts with the natural numbers, then the positive integers, then the integers, then the rational numbers, then the reals etc. This is very normal for high-school level maths education.

I believe that mathematically the formal theory of types comes from a different branch from sets which arose when Russel attempted to address the problems caused by his paradox. "Type" theory was part of Russel's solution whereas Zermelo Fraenkel set theory is where everyone else felt that sets just needed a little patch to carry on working pretty much as before.

[1] Which I'd really recommend for anyone who wants a maths refresher that starts from very basic concepts but really challenges you to think like a mathematician, prove things etc. So in the first chapter when you only know the distributive and associative properties he has you using them to prove stuff.

As a sibling comment observed, you would be proving something about a program, but proving things about programs is both possible and done.

This ranges from things like CakeML (https://cakeml.org/) and CompCert (compilers with verified correctness proofs of their optimizations) to something simple like absence of runtime type errors in statically strongly soundly-typed languages.

Of note is that you are proving properties of your program, not proving them perfect in every way. The properties of your program that you prove can vary wildly in both difficulty and usefulness. A sufficiently advanced formally verified compiler like CakeML can transfer a high-level proof about your source code to a corresponding proof about the behavior of the generated machine-executable code.

"One way to resolve the paradox, therefore, is to put these types into a hierarchy, so they can only contain elements of a “lower level” than themselves. Then a type can’t contain itself, which avoids the self-referentiality that creates the paradox."

This is similar to constraints of making something semi-decidable or recursively enumerable.

Provable, recursively enumerable, semidecidable, and turing recognizable are all the same thing described in different ways.

Some things are easier to find in type theory, other in set theory and for some Turing machines work better.

The Church–Turing thesis isn't provable but is the safe assumption.

IMHO termination analysis, which will never be complete, has more interesting and has some implications for ATP that aren't as easily captured in type theory.

As an example related to term rewriting which will be important to ML.

https://arxiv.org/abs/2307.14805

However, this is not what the article is about. Instead, it talks about an interesting observation that there is a direct correspondence between a certain kind of program and a mathematical proof, and also between the type of the program, and the theorem validated by the proof. In other words, you can think of mathematical proofs as computational objects. The intuition for the correspondence is not hard: for example, support I want to prove that "if A is true, then B must also be true". You may think of a proof for such a property as a program, which takes as input a proof that `A` holds, and as its output produces a proof that `B` holds.

The point being is there is no single general algorithm that can solve them.

The example you gave above is propositional logic, or zeroith order logic which is known to be decidable.

First order logic and higher order logic are not decidable.

Total functions are also not subject to the halting problem, but unfortunately finding a total function in the general case is also undecidable.

And yes we can prove termination and zero bugs for a lot of practical useful code. Examples: seL4 is a proven correct micro kernel and CompCert is a proven correct C compiler.

The trick is to use programming languages that are total i.e. not general infinite tape turing machines.

In principle, nothing prevents you from taking e.g. an ARM binary and formally proving that it will never crash in some environment, e.g., bare metal chip with known amounts of memory etc. This is very hard for useful programs and not worth it in pretty much any application there ever was, but it's possible and getting ever easier over time.

It also isn't clear that the machines itself actually do what they say, though hardware is a lot more likely to be mathematically proven.

Maybe that's a nitpick, but I would say it's fundamentally impossible to mathematically prove anything at all about a physical system. You have to assume some model to do the proof and have no way of ever "proving" (what would that even mean?) that model.

I guess you're referring to the fact that verification and formal methods are used in hardware more often than software. This is due to commercial reasons: you can't just reprogram a million chips once they leave your fab.

What you mean is that it's practically infeasible to verify every program behaviour we're interested in. That's probably true for large enough programs, but it doesn't mean we can prove nothing about them.

I don’t think this is true, something as “trivial” as halting already can’t be proven in the general case.

And the number of possible states increase so fast that you might as well think of it as infinite.

Gödell showed there are algorithms that we cannot prove, but he did that with self referencing algorithms which we rarely use.

Still, you can’t even in theory prove every interesting property about any problem/algorithm.

A typical theory says:

For all x:A, P x

In other words, given any x (from an infinite set A) P x is true. Where P is a proposition.

You typically prove it using straightforward induction/recursion.

Of course, what you are saying about “stronger systems can prove the answers to the questions of the whether the machines from larger sets, halt” is also true, I just, wouldn’t describe this as “the halting problem”, even though they are I guess basically equivalent.

I assume mostly known in this site.

thought I guess you mean something more top-downish? for that there's "program interpretation" ( https://github.com/AdrielC/free-arrow )

and this just looks very interesting https://deepai.org/publication/a-coq-based-synthesis-of-scal...

And no. Ada is an imperative language with an expressive type system (especially compared to other imperative languages). But it doesn't require things like mathematical correctness/completeness. You may be thinking of SPARK which is a subset of Ada that uses contracts and a prover to prove the contracts hold.

That will allow you to verify the pure functions. It will not verify the input/output that will also be necessary.

"Dikestra" has a shorter path to the Dutch pronunciation than Djikstra.

Obviously the above is a very truncated list and misses out on a huge chunk of formative thinkers, and doesn’t get to the cutting edge modern developments. Additionally, I’m leaving out the Math centric developments and people, like Mike Shulman, Dan Licata, etc.

It does have something to do with his work because his work extended it. But by that metric, it also has something to do with all of computer science, and a lot of mathematics.

  Finally, a word or two about a wide-spread superstition, viz. that correctness proofs can only be given if you know exactly what your program has to do, that in real life it is often not completely known what the program has to do and that, therefore, in real life correctness proofs are impractical. The fallacy in this argument is to be found in the confusion between "exact" and "complete": although the program requirements may still be "incomplete", a certain number of broad characteristics will be "exactly" known. The abstract program can see to it that these broad specifications are exactly met, while more detailed aspects of the problem specification are catered for in the lower levels.

Edit: I find it amusing how much closer Dijkstra's approach is to what might be called "normal" (Algol-ish) programming compared to the Abstract Nonsense[5] favored by the category theorists. I wouldn't call it any less mathematical though. Dijkstra was very much a mathematical formalist as is clear to anyone who has made a study of his work or life.

[1] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD02xx/E...

[2] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD03xx/E...

[3] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD08xx/E...

[4] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD11xx/E...

[5] https://en.wikipedia.org/wiki/Abstract_nonsense

It's true that he mainly used a sequential, imperative notation for describing things, but it seems like later in his life, he preferred functional programming for teaching computer science to students. He petitioned the University of Texas to not switch from teaching it in Haskell to teaching it in Java for this reason.

https://www.cs.utexas.edu/users/EWD/OtherDocs/To%20the%20Bud...

A fundamental reason for the preference is that functional programs are much more readily appreciated as mathematical objects than imperative ones, so that you can teach what rigorous reasoning about programs amounts to. The additional advantage of functional programming with “lazy evaluation” is that it provides an environment that discourages operational reasoning.

You don't need curry-howard for software verification, you don't need it for mathematics, and you don't need it for logic.

You only really need it to j*rk off hard over types.

At the lowest machine level, a computer program is simply base 2 math --- the simplest possible number system --- aka binary logic.

Aside from moving mathematical data around in storage, math is really about the *only* thing a computer processor does.

Yes, programming is a super set of theorem proving.

It is true, but not generally useful.

Building useful programmes is, IMO, best described as a craft. It is learnt from other crafters, and improves with practice

Formal methods can be helpful in specific cases but generally speaking writing correct formal specifications is just as hard, or harder, than writing useful, reliable, computer programs